Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > abbii | Unicode version |
Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abbii.1 |
Ref | Expression |
---|---|
abbii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbi 2278 | . 2 | |
2 | abbii.1 | . 2 | |
3 | 1, 2 | mpgbi 1439 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wceq 1342 cab 2150 |
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 |
This theorem is referenced by: rabswap 2642 rabbiia 2706 rabab 2742 csb2 3042 cbvcsbw 3044 cbvcsb 3045 csbid 3048 csbco 3050 csbcow 3051 cbvreucsf 3104 unrab 3388 inrab 3389 inrab2 3390 difrab 3391 rabun2 3396 dfnul3 3407 rab0 3432 tprot 3663 pw0 3714 dfuni2 3785 unipr 3797 dfint2 3820 int0 3832 dfiunv2 3896 cbviun 3897 cbviin 3898 iunrab 3907 iunid 3915 viin 3919 cbvopab 4047 cbvopab1 4049 cbvopab2 4050 cbvopab1s 4051 cbvopab2v 4053 unopab 4055 iunopab 4253 abnex 4419 uniuni 4423 ruv 4521 rabxp 4635 dfdm3 4785 dfrn2 4786 dfrn3 4787 dfdm4 4790 dfdmf 4791 dmun 4805 dmopab 4809 dmopabss 4810 dmopab3 4811 dfrnf 4839 rnopab 4845 rnmpt 4846 dfima2 4942 dfima3 4943 imadmrn 4950 imai 4954 args 4967 mptpreima 5091 dfiota2 5148 cbviota 5152 sb8iota 5154 dffv4g 5477 dfimafn2 5530 fnasrn 5657 fnasrng 5659 elabrex 5720 abrexco 5721 dfoprab2 5880 cbvoprab2 5906 dmoprab 5914 rnoprab 5916 rnoprab2 5917 fnrnov 5978 abrexex2g 6080 abrexex2 6084 abexssex 6085 abexex 6086 oprabrexex2 6090 dfopab2 6149 cnvoprab 6193 tfr1onlemaccex 6307 tfrcllemaccex 6320 tfrcldm 6322 frec0g 6356 frecsuc 6366 snec 6553 pmex 6610 dfixp 6657 cbvixp 6672 caucvgprprlemmu 7627 caucvgsr 7734 pitonnlem1 7777 mertenslem2 11463 toponsspwpwg 12567 tgval2 12598 if0ab 13528 bdcuni 13599 bj-dfom 13656 |
Copyright terms: Public domain | W3C validator |