![]() |
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 1541 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | exbii.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpg 1386 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-ial 1473 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2exbii 1543 3exbii 1544 exancom 1545 excom13 1625 exrot4 1627 eeor 1631 sbcof2 1739 sbequ8 1776 sbidm 1780 sborv 1819 19.41vv 1832 19.41vvv 1833 19.41vvvv 1834 exdistr 1836 19.42vvv 1838 exdistr2 1840 3exdistr 1841 4exdistr 1842 eean 1855 eeeanv 1857 ee4anv 1858 2sb5 1908 2sb5rf 1914 sbel2x 1923 sbexyz 1928 sbex 1929 exsb 1933 2exsb 1934 sb8eu 1962 sb8euh 1972 eu1 1974 eu2 1993 2moswapdc 2039 2exeu 2041 exists1 2045 clelab 2213 clabel 2214 sbabel 2255 rexbii2 2390 r2exf 2397 nfrexdya 2414 r19.41 2523 r19.43 2526 isset 2626 rexv 2638 ceqsex2 2660 ceqsex3v 2662 gencbvex 2666 ceqsrexv 2748 rexab 2778 rexrab2 2783 euxfrdc 2802 euind 2803 reu6 2805 reu3 2806 2reuswapdc 2820 reuind 2821 sbccomlem 2914 rmo2ilem 2929 rexun 3181 reupick3 3285 abn0r 3311 abn0m 3312 rabn0m 3314 rexsns 3486 exsnrex 3489 snprc 3511 euabsn2 3515 reusn 3517 eusn 3520 elunirab 3672 unipr 3673 uniun 3678 uniin 3679 iuncom4 3743 dfiun2g 3768 iunn0m 3796 iunxiun 3816 disjnim 3842 cbvopab2 3918 cbvopab2v 3921 unopab 3923 zfnuleu 3969 0ex 3972 vnex 3976 inex1 3979 intexabim 3994 iinexgm 3996 inuni 3997 unidif0 4008 axpweq 4012 zfpow 4016 axpow2 4017 axpow3 4018 vpwex 4020 zfpair2 4046 mss 4062 exss 4063 opm 4070 eqvinop 4079 copsexg 4080 opabm 4116 iunopab 4117 zfun 4270 uniex2 4272 uniuni 4286 rexxfrd 4298 dtruex 4388 zfinf2 4417 elxp2 4470 opeliunxp 4506 xpiundi 4509 xpiundir 4510 elvvv 4514 eliunxp 4588 rexiunxp 4591 relop 4599 elco 4615 opelco2g 4617 cnvco 4634 cnvuni 4635 dfdm3 4636 dfrn2 4637 dfrn3 4638 elrng 4640 dfdm4 4641 eldm2g 4645 dmun 4656 dmin 4657 dmiun 4658 dmuni 4659 dmopab 4660 dmi 4664 dmmrnm 4668 elrn 4691 rnopab 4695 dmcosseq 4717 dmres 4747 elres 4761 elsnres 4762 dfima2 4789 elima3 4794 imadmrn 4797 imai 4801 args 4814 rniun 4855 ssrnres 4886 dmsnm 4909 dmsnopg 4915 elxp4 4931 elxp5 4932 cnvresima 4933 mptpreima 4937 dfco2 4943 coundi 4945 coundir 4946 resco 4948 imaco 4949 rnco 4950 coiun 4953 coi1 4959 coass 4962 xpcom 4990 dffun2 5038 imadif 5107 imainlem 5108 funimaexglem 5110 fun11iun 5287 f11o 5299 brprcneu 5311 nfvres 5350 fndmin 5420 abrexco 5552 imaiun 5553 dfoprab2 5710 cbvoprab2 5735 rexrnmpt2 5774 opabex3d 5906 opabex3 5907 abexssex 5910 abexex 5911 oprabrexex2 5915 releldm2 5969 dfopab2 5973 dfoprab3s 5974 cnvoprab 6013 brtpos2 6030 tfr1onlemaccex 6127 tfrcllembxssdm 6135 tfrcllemaccex 6140 domen 6522 mapsnen 6582 xpsnen 6591 xpcomco 6596 xpassen 6600 fimax2gtri 6671 supelti 6751 subhalfnqq 7034 ltbtwnnq 7036 prnmaxl 7108 prnminu 7109 prarloc 7123 genpdflem 7127 genpassl 7144 genpassu 7145 ltexprlemm 7220 2rexuz 9131 seq3f1olemp 9992 cbvsum 10810 isbasis2g 11804 tgval2 11812 ntreq0 11893 bj-axempty 12057 bj-axempty2 12058 bj-vprc 12060 bdinex1 12063 bj-zfpair2 12074 bj-uniex2 12080 bj-d0clsepcl 12093 |
Copyright terms: Public domain | W3C validator |