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 2164 | . 2 | |
2 | opabbii.1 | . . . 4 | |
3 | 2 | a1i 9 | . . 3 |
4 | 3 | opabbidv 4042 | . 2 |
5 | 1, 4 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wceq 1342 copab 4036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-opab 4038 |
This theorem is referenced by: mptv 4073 fconstmpt 4645 xpundi 4654 xpundir 4655 inxp 4732 cnvco 4783 resopab 4922 opabresid 4931 cnvi 5002 cnvun 5003 cnvin 5005 cnvxp 5016 cnvcnv3 5047 coundi 5099 coundir 5100 mptun 5313 fvopab6 5576 cbvoprab1 5905 cbvoprab12 5907 dmoprabss 5915 mpomptx 5924 resoprab 5929 ov6g 5970 dfoprab3s 6150 dfoprab3 6151 dfoprab4 6152 mapsncnv 6652 xpcomco 6783 dmaddpq 7311 dmmulpq 7312 recmulnqg 7323 enq0enq 7363 ltrelxr 7950 ltxr 9702 shftidt2 10760 lmfval 12739 lmbr 12760 cnmptid 12828 |
Copyright terms: Public domain | W3C validator |