New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > abbidv | Unicode version |
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.) |
Ref | Expression |
---|---|
abbidv.1 |
Ref | Expression |
---|---|
abbidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 | |
2 | abbidv.1 | . 2 | |
3 | 1, 2 | abbid 2467 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wceq 1642 cab 2339 |
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 |
This theorem is referenced by: csbeq1 3140 sbcel12g 3152 sbceqg 3153 csbeq2d 3161 csbnestgf 3185 nineq1 3235 pweq 3726 sneq 3745 csbsng 3786 rabsn 3791 csbunig 3900 unieq 3901 inteq 3930 iineq1 3984 iineq2 3987 dfiin2g 4001 iinrab 4029 cnvkeq 4216 ins2keq 4219 ins3keq 4220 imakeq1 4225 imakeq2 4226 p6eq 4239 sikeq 4242 setswith 4322 iotaeq 4348 iotabi 4349 preaddccan2lem1 4455 nnadjoin 4521 tfinnn 4535 opabbid 4625 csbxpg 4814 imaeq1 4938 imaeq2 4939 csbrng 4967 imasn 5019 fnrnfv 5365 dfimafn 5367 fnsnfv 5374 fvco2 5383 oprabbid 5564 clos1eq1 5875 clos1eq2 5876 erth 5969 qseq1 5975 qseq2 5976 mapex 6007 mapvalg 6010 ovmuc 6131 ovce 6173 addccan2nclem2 6265 |
Copyright terms: Public domain | W3C validator |