![]() |
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 1615 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | |
2 | exbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1462 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∃wex 1503 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 2exbii 1617 3exbii 1618 exancom 1619 excom13 1700 exrot4 1702 eeor 1706 sbcof2 1821 sbequ8 1858 sbidm 1862 sborv 1902 19.41vv 1915 19.41vvv 1916 19.41vvvv 1917 exdistr 1921 19.42vvv 1924 exdistr2 1926 3exdistr 1927 4exdistr 1928 eean 1943 eeeanv 1945 ee4anv 1946 2sb5 1995 2sb5rf 2001 sbel2x 2010 sbexyz 2015 sbex 2016 exsb 2020 2exsb 2021 sb8eu 2051 sb8euh 2061 eu1 2063 eu2 2082 2moswapdc 2128 2exeu 2130 exists1 2134 clelab 2315 clabel 2316 sbabel 2359 rexbii2 2501 r2exf 2508 nfrexdya 2526 r19.41 2645 r19.43 2648 cbvreuvw 2724 isset 2758 rexv 2770 ceqsex2 2792 ceqsex3v 2794 gencbvex 2798 ceqsrexv 2882 rexab 2914 rexrab2 2919 euxfrdc 2938 euind 2939 reu6 2941 reu3 2942 2reuswapdc 2956 reuind 2957 sbccomlem 3052 rmo2ilem 3067 rexun 3330 reupick3 3435 abn0r 3462 abn0m 3463 rabn0m 3465 rexsns 3646 exsnrex 3649 snprc 3672 euabsn2 3676 reusn 3678 eusn 3681 elunirab 3837 unipr 3838 uniun 3843 uniin 3844 iuncom4 3908 dfiun2g 3933 iunn0m 3962 iunxiun 3983 disjnim 4009 cbvopab2 4092 cbvopab2v 4095 unopab 4097 zfnuleu 4142 0ex 4145 vnex 4149 inex1 4152 intexabim 4167 iinexgm 4169 inuni 4170 unidif0 4182 axpweq 4186 zfpow 4190 axpow2 4191 axpow3 4192 vpwex 4194 zfpair2 4225 mss 4241 exss 4242 opm 4249 eqvinop 4258 copsexg 4259 opabm 4295 iunopab 4296 zfun 4449 uniex2 4451 uniuni 4466 rexxfrd 4478 dtruex 4573 zfinf2 4603 elxp2 4659 opeliunxp 4696 xpiundi 4699 xpiundir 4700 elvvv 4704 eliunxp 4781 rexiunxp 4784 relop 4792 elco 4808 opelco2g 4810 cnvco 4827 cnvuni 4828 dfdm3 4829 dfrn2 4830 dfrn3 4831 elrng 4833 dfdm4 4834 eldm2g 4838 dmun 4849 dmin 4850 dmiun 4851 dmuni 4852 dmopab 4853 dmi 4857 dmmrnm 4861 elrn 4885 rnopab 4889 dmcosseq 4913 dmres 4943 elres 4958 elsnres 4959 dfima2 4987 elima3 4992 imadmrn 4995 imai 4999 args 5012 rniun 5054 ssrnres 5086 dmsnm 5109 dmsnopg 5115 elxp4 5131 elxp5 5132 cnvresima 5133 mptpreima 5137 dfco2 5143 coundi 5145 coundir 5146 resco 5148 imaco 5149 rnco 5150 coiun 5153 coi1 5159 coass 5162 xpcom 5190 dffun2 5242 imadif 5312 imainlem 5313 funimaexglem 5315 fun11iun 5498 f11o 5510 brprcneu 5524 nfvres 5564 fndmin 5640 abrexco 5777 imaiun 5778 dfoprab2 5939 cbvoprab2 5965 rexrnmpo 6008 opabex3d 6141 opabex3 6142 abexssex 6145 abexex 6146 oprabrexex2 6150 releldm2 6205 dfopab2 6209 dfoprab3s 6210 cnvoprab 6254 brtpos2 6271 tfr1onlemaccex 6368 tfrcllembxssdm 6376 tfrcllemaccex 6381 domen 6772 mapsnen 6832 xpsnen 6842 xpcomco 6847 xpassen 6851 fimax2gtri 6924 supelti 7026 cc1 7289 subhalfnqq 7438 ltbtwnnq 7440 prnmaxl 7512 prnminu 7513 prarloc 7527 genpdflem 7531 genpassl 7548 genpassu 7549 ltexprlemm 7624 2rexuz 9607 seq3f1olemp 10528 cbvsum 11395 cbvprod 11593 nnwosdc 12067 4sqlem12 12429 inffinp1 12475 ctiunctal 12487 unct 12488 isbasis2g 13982 tgval2 13988 ntreq0 14069 lmff 14186 metrest 14443 bj-axempty 15082 bj-axempty2 15083 bj-vprc 15085 bdinex1 15088 bj-zfpair2 15099 bj-uniex2 15105 bj-d0clsepcl 15114 |
Copyright terms: Public domain | W3C validator |