New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 2353 | . 2 | |
2 | opabbii.1 | . . . 4 | |
3 | 2 | a1i 10 | . . 3 |
4 | 3 | opabbidv 4625 | . 2 |
5 | 1, 4 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wceq 1642 copab 4622 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-opab 4623 |
This theorem is referenced by: df1st2 4738 dfsset2 4743 dfco1 4748 dfsi2 4751 fconstopab 4815 xpundi 4832 xpundir 4833 inxp 4863 opabbi2i 4866 cnvco 4894 resopab 4999 opabresid 5003 cnvi 5032 cnvun 5033 cnvxp 5043 coundi 5082 coundir 5083 df2nd2 5111 fvopabg 5391 cbvoprab1 5567 cbvoprab12 5569 dmoprabss 5575 resoprab 5581 fnov 5591 ov6g 5600 mpt2mptx 5708 mptv 5718 scancan 6331 |
Copyright terms: Public domain | W3C validator |