![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exbii | GIF 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 1604 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | |
2 | exbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1451 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 2exbii 1606 3exbii 1607 exancom 1608 excom13 1689 exrot4 1691 eeor 1695 sbcof2 1810 sbequ8 1847 sbidm 1851 sborv 1890 19.41vv 1903 19.41vvv 1904 19.41vvvv 1905 exdistr 1909 19.42vvv 1912 exdistr2 1914 3exdistr 1915 4exdistr 1916 eean 1931 eeeanv 1933 ee4anv 1934 2sb5 1983 2sb5rf 1989 sbel2x 1998 sbexyz 2003 sbex 2004 exsb 2008 2exsb 2009 sb8eu 2039 sb8euh 2049 eu1 2051 eu2 2070 2moswapdc 2116 2exeu 2118 exists1 2122 clelab 2303 clabel 2304 sbabel 2346 rexbii2 2488 r2exf 2495 nfrexdya 2513 r19.41 2632 r19.43 2635 cbvreuvw 2709 isset 2743 rexv 2755 ceqsex2 2777 ceqsex3v 2779 gencbvex 2783 ceqsrexv 2867 rexab 2899 rexrab2 2904 euxfrdc 2923 euind 2924 reu6 2926 reu3 2927 2reuswapdc 2941 reuind 2942 sbccomlem 3037 rmo2ilem 3052 rexun 3315 reupick3 3420 abn0r 3447 abn0m 3448 rabn0m 3450 rexsns 3630 exsnrex 3633 snprc 3656 euabsn2 3660 reusn 3662 eusn 3665 elunirab 3820 unipr 3821 uniun 3826 uniin 3827 iuncom4 3891 dfiun2g 3916 iunn0m 3944 iunxiun 3965 disjnim 3991 cbvopab2 4074 cbvopab2v 4077 unopab 4079 zfnuleu 4124 0ex 4127 vnex 4131 inex1 4134 intexabim 4149 iinexgm 4151 inuni 4152 unidif0 4164 axpweq 4168 zfpow 4172 axpow2 4173 axpow3 4174 vpwex 4176 zfpair2 4207 mss 4223 exss 4224 opm 4231 eqvinop 4240 copsexg 4241 opabm 4277 iunopab 4278 zfun 4431 uniex2 4433 uniuni 4448 rexxfrd 4460 dtruex 4555 zfinf2 4585 elxp2 4641 opeliunxp 4678 xpiundi 4681 xpiundir 4682 elvvv 4686 eliunxp 4762 rexiunxp 4765 relop 4773 elco 4789 opelco2g 4791 cnvco 4808 cnvuni 4809 dfdm3 4810 dfrn2 4811 dfrn3 4812 elrng 4814 dfdm4 4815 eldm2g 4819 dmun 4830 dmin 4831 dmiun 4832 dmuni 4833 dmopab 4834 dmi 4838 dmmrnm 4842 elrn 4866 rnopab 4870 dmcosseq 4894 dmres 4924 elres 4939 elsnres 4940 dfima2 4968 elima3 4973 imadmrn 4976 imai 4980 args 4993 rniun 5035 ssrnres 5067 dmsnm 5090 dmsnopg 5096 elxp4 5112 elxp5 5113 cnvresima 5114 mptpreima 5118 dfco2 5124 coundi 5126 coundir 5127 resco 5129 imaco 5130 rnco 5131 coiun 5134 coi1 5140 coass 5143 xpcom 5171 dffun2 5222 imadif 5292 imainlem 5293 funimaexglem 5295 fun11iun 5478 f11o 5490 brprcneu 5504 nfvres 5544 fndmin 5619 abrexco 5754 imaiun 5755 dfoprab2 5916 cbvoprab2 5942 rexrnmpo 5984 opabex3d 6116 opabex3 6117 abexssex 6120 abexex 6121 oprabrexex2 6125 releldm2 6180 dfopab2 6184 dfoprab3s 6185 cnvoprab 6229 brtpos2 6246 tfr1onlemaccex 6343 tfrcllembxssdm 6351 tfrcllemaccex 6356 domen 6745 mapsnen 6805 xpsnen 6815 xpcomco 6820 xpassen 6824 fimax2gtri 6895 supelti 6995 cc1 7252 subhalfnqq 7401 ltbtwnnq 7403 prnmaxl 7475 prnminu 7476 prarloc 7490 genpdflem 7494 genpassl 7511 genpassu 7512 ltexprlemm 7587 2rexuz 9568 seq3f1olemp 10485 cbvsum 11349 cbvprod 11547 nnwosdc 12020 inffinp1 12410 ctiunctal 12422 unct 12423 isbasis2g 13203 tgval2 13211 ntreq0 13292 lmff 13409 metrest 13666 bj-axempty 14294 bj-axempty2 14295 bj-vprc 14297 bdinex1 14300 bj-zfpair2 14311 bj-uniex2 14317 bj-d0clsepcl 14326 |
Copyright terms: Public domain | W3C validator |