Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > opabbii | Unicode version |
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbii.1 |
Ref | Expression |
---|---|
opabbii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2040 | . 2 | |
2 | opabbii.1 | . . . 4 | |
3 | 2 | a1i 9 | . . 3 |
4 | 3 | opabbidv 3823 | . 2 |
5 | 1, 4 | ax-mp 7 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 98 wceq 1243 copab 3817 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-opab 3819 |
This theorem is referenced by: mptv 3853 fconstmpt 4387 xpundi 4396 xpundir 4397 inxp 4470 cnvco 4520 resopab 4652 opabresid 4659 cnvi 4728 cnvun 4729 cnvin 4731 cnvxp 4742 cnvcnv3 4770 coundi 4822 coundir 4823 mptun 5029 fvopab6 5264 cbvoprab1 5576 cbvoprab12 5578 dmoprabss 5586 mpt2mptx 5595 resoprab 5597 ov6g 5638 dfoprab3s 5816 dfoprab3 5817 dfoprab4 5818 xpcomco 6300 dmaddpq 6477 dmmulpq 6478 recmulnqg 6489 enq0enq 6529 ltrelxr 7080 ltxr 8695 shftidt2 9433 |
Copyright terms: Public domain | W3C validator |