![]() |
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 rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
abbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbi 2196 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | abbii.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpgbi 1382 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 |
This theorem is referenced by: rabswap 2538 rabbiia 2597 rabab 2631 csb2 2921 cbvcsb 2923 csbid 2926 csbco 2928 cbvreucsf 2977 unrab 3253 inrab 3254 inrab2 3255 difrab 3256 rabun2 3261 dfnul3 3272 rab0 3294 tprot 3509 pw0 3558 dfuni2 3629 unipr 3641 dfint2 3664 int0 3676 dfiunv2 3740 cbviun 3741 cbviin 3742 iunrab 3751 iunid 3759 viin 3763 cbvopab 3875 cbvopab1 3877 cbvopab2 3878 cbvopab1s 3879 cbvopab2v 3881 unopab 3883 iunopab 4072 uniuni 4237 ruv 4329 rabxp 4436 dfdm3 4581 dfrn2 4582 dfrn3 4583 dfdm4 4586 dfdmf 4587 dmun 4601 dmopab 4605 dmopabss 4606 dmopab3 4607 dfrnf 4634 rnopab 4640 rnmpt 4641 dfima2 4731 dfima3 4732 imadmrn 4739 imai 4743 args 4756 mptpreima 4878 dfiota2 4935 cbviota 4939 sb8iota 4941 dffv4g 5250 dfimafn2 5299 fnasrn 5417 fnasrng 5419 elabrex 5477 abrexco 5478 dfoprab2 5631 cbvoprab2 5656 dmoprab 5664 rnoprab 5666 rnoprab2 5667 fnrnov 5725 abrexex2g 5826 abrexex2 5830 abexssex 5831 abexex 5832 oprabrexex2 5836 dfopab2 5894 cnvoprab 5934 tfr1onlemaccex 6045 tfrcllemaccex 6058 tfrcldm 6060 frec0g 6094 frecsuc 6104 snec 6283 pmex 6340 caucvgprprlemmu 7157 caucvgsr 7250 pitonnlem1 7285 bdcuni 11110 bj-dfom 11171 |
Copyright terms: Public domain | W3C validator |