![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exbii | Unicode version |
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Ref | Expression |
---|---|
exbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbi 1540 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | exbii.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpg 1385 |
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 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-ial 1472 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 2exbii 1542 3exbii 1543 exancom 1544 excom13 1624 exrot4 1626 eeor 1630 sbcof2 1738 sbequ8 1775 sbidm 1779 sborv 1818 19.41vv 1831 19.41vvv 1832 19.41vvvv 1833 exdistr 1835 19.42vvv 1837 exdistr2 1839 3exdistr 1840 4exdistr 1841 eean 1854 eeeanv 1856 ee4anv 1857 2sb5 1907 2sb5rf 1913 sbel2x 1922 sbexyz 1927 sbex 1928 exsb 1932 2exsb 1933 sb8eu 1961 sb8euh 1971 eu1 1973 eu2 1992 2moswapdc 2038 2exeu 2040 exists1 2044 clelab 2212 clabel 2213 sbabel 2254 rexbii2 2389 r2exf 2396 nfrexdya 2413 r19.41 2522 r19.43 2525 isset 2625 rexv 2637 ceqsex2 2659 ceqsex3v 2661 gencbvex 2665 ceqsrexv 2747 rexab 2777 rexrab2 2782 euxfrdc 2801 euind 2802 reu6 2804 reu3 2805 2reuswapdc 2819 reuind 2820 sbccomlem 2913 rmo2ilem 2928 rexun 3180 reupick3 3284 abn0r 3307 abn0m 3308 rabn0m 3310 rexsns 3482 exsnrex 3485 snprc 3507 euabsn2 3511 reusn 3513 eusn 3516 elunirab 3666 unipr 3667 uniun 3672 uniin 3673 iuncom4 3737 dfiun2g 3762 iunn0m 3790 iunxiun 3810 disjnim 3836 cbvopab2 3912 cbvopab2v 3915 unopab 3917 zfnuleu 3963 0ex 3966 vnex 3970 inex1 3973 intexabim 3988 iinexgm 3990 inuni 3991 unidif0 4002 axpweq 4006 zfpow 4010 axpow2 4011 axpow3 4012 vpwex 4014 zfpair2 4037 mss 4053 exss 4054 opm 4061 eqvinop 4070 copsexg 4071 opabm 4107 iunopab 4108 zfun 4261 uniex2 4263 uniuni 4273 rexxfrd 4285 dtruex 4375 zfinf2 4404 elxp2 4456 opeliunxp 4493 xpiundi 4496 xpiundir 4497 elvvv 4501 eliunxp 4575 rexiunxp 4578 relop 4586 elco 4602 opelco2g 4604 cnvco 4621 cnvuni 4622 dfdm3 4623 dfrn2 4624 dfrn3 4625 elrng 4627 dfdm4 4628 eldm2g 4632 dmun 4643 dmin 4644 dmiun 4645 dmuni 4646 dmopab 4647 dmi 4651 dmmrnm 4655 elrn 4678 rnopab 4682 dmcosseq 4704 dmres 4734 elres 4748 elsnres 4749 dfima2 4776 elima3 4781 imadmrn 4784 imai 4788 args 4801 rniun 4842 ssrnres 4873 dmsnm 4896 dmsnopg 4902 elxp4 4918 elxp5 4919 cnvresima 4920 mptpreima 4924 dfco2 4930 coundi 4932 coundir 4933 resco 4935 imaco 4936 rnco 4937 coiun 4940 coi1 4946 coass 4949 xpcom 4977 dffun2 5025 imadif 5094 imainlem 5095 funimaexglem 5097 fun11iun 5274 f11o 5286 brprcneu 5298 nfvres 5337 fndmin 5406 abrexco 5538 imaiun 5539 dfoprab2 5696 cbvoprab2 5721 rexrnmpt2 5760 opabex3d 5892 opabex3 5893 abexssex 5896 abexex 5897 oprabrexex2 5901 releldm2 5955 dfopab2 5959 dfoprab3s 5960 cnvoprab 5999 brtpos2 6016 tfr1onlemaccex 6113 tfrcllembxssdm 6121 tfrcllemaccex 6126 domen 6468 mapsnen 6528 xpsnen 6537 xpcomco 6542 xpassen 6546 fimax2gtri 6617 supelti 6697 subhalfnqq 6973 ltbtwnnq 6975 prnmaxl 7047 prnminu 7048 prarloc 7062 genpdflem 7066 genpassl 7083 genpassu 7084 ltexprlemm 7159 2rexuz 9070 seq3f1olemp 9931 cbvsum 10749 bj-axempty 11784 bj-axempty2 11785 bj-vprc 11787 bdinex1 11790 bj-zfpair2 11801 bj-uniex2 11807 bj-d0clsepcl 11820 |
Copyright terms: Public domain | W3C validator |