![]() |
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 1566 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | |
2 | exbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1410 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∃wex 1451 |
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 1406 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-4 1470 ax-ial 1497 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2exbii 1568 3exbii 1569 exancom 1570 excom13 1650 exrot4 1652 eeor 1656 sbcof2 1764 sbequ8 1801 sbidm 1805 sborv 1844 19.41vv 1857 19.41vvv 1858 19.41vvvv 1859 exdistr 1861 19.42vvv 1864 exdistr2 1866 3exdistr 1867 4exdistr 1868 eean 1881 eeeanv 1883 ee4anv 1884 2sb5 1934 2sb5rf 1940 sbel2x 1949 sbexyz 1954 sbex 1955 exsb 1959 2exsb 1960 sb8eu 1988 sb8euh 1998 eu1 2000 eu2 2019 2moswapdc 2065 2exeu 2067 exists1 2071 clelab 2239 clabel 2240 sbabel 2281 rexbii2 2420 r2exf 2427 nfrexdya 2444 r19.41 2560 r19.43 2563 isset 2663 rexv 2675 ceqsex2 2697 ceqsex3v 2699 gencbvex 2703 ceqsrexv 2785 rexab 2815 rexrab2 2820 euxfrdc 2839 euind 2840 reu6 2842 reu3 2843 2reuswapdc 2857 reuind 2858 sbccomlem 2951 rmo2ilem 2966 rexun 3222 reupick3 3327 abn0r 3353 abn0m 3354 rabn0m 3356 rexsns 3529 exsnrex 3532 snprc 3554 euabsn2 3558 reusn 3560 eusn 3563 elunirab 3715 unipr 3716 uniun 3721 uniin 3722 iuncom4 3786 dfiun2g 3811 iunn0m 3839 iunxiun 3860 disjnim 3886 cbvopab2 3962 cbvopab2v 3965 unopab 3967 zfnuleu 4012 0ex 4015 vnex 4019 inex1 4022 intexabim 4037 iinexgm 4039 inuni 4040 unidif0 4051 axpweq 4055 zfpow 4059 axpow2 4060 axpow3 4061 vpwex 4063 zfpair2 4092 mss 4108 exss 4109 opm 4116 eqvinop 4125 copsexg 4126 opabm 4162 iunopab 4163 zfun 4316 uniex2 4318 uniuni 4332 rexxfrd 4344 dtruex 4434 zfinf2 4463 elxp2 4517 opeliunxp 4554 xpiundi 4557 xpiundir 4558 elvvv 4562 eliunxp 4638 rexiunxp 4641 relop 4649 elco 4665 opelco2g 4667 cnvco 4684 cnvuni 4685 dfdm3 4686 dfrn2 4687 dfrn3 4688 elrng 4690 dfdm4 4691 eldm2g 4695 dmun 4706 dmin 4707 dmiun 4708 dmuni 4709 dmopab 4710 dmi 4714 dmmrnm 4718 elrn 4742 rnopab 4746 dmcosseq 4768 dmres 4798 elres 4813 elsnres 4814 dfima2 4841 elima3 4846 imadmrn 4849 imai 4853 args 4866 rniun 4907 ssrnres 4939 dmsnm 4962 dmsnopg 4968 elxp4 4984 elxp5 4985 cnvresima 4986 mptpreima 4990 dfco2 4996 coundi 4998 coundir 4999 resco 5001 imaco 5002 rnco 5003 coiun 5006 coi1 5012 coass 5015 xpcom 5043 dffun2 5091 imadif 5161 imainlem 5162 funimaexglem 5164 fun11iun 5344 f11o 5356 brprcneu 5368 nfvres 5408 fndmin 5481 abrexco 5614 imaiun 5615 dfoprab2 5772 cbvoprab2 5798 rexrnmpo 5840 opabex3d 5973 opabex3 5974 abexssex 5977 abexex 5978 oprabrexex2 5982 releldm2 6037 dfopab2 6041 dfoprab3s 6042 cnvoprab 6085 brtpos2 6102 tfr1onlemaccex 6199 tfrcllembxssdm 6207 tfrcllemaccex 6212 domen 6599 mapsnen 6659 xpsnen 6668 xpcomco 6673 xpassen 6677 fimax2gtri 6748 supelti 6841 subhalfnqq 7170 ltbtwnnq 7172 prnmaxl 7244 prnminu 7245 prarloc 7259 genpdflem 7263 genpassl 7280 genpassu 7281 ltexprlemm 7356 2rexuz 9279 seq3f1olemp 10168 cbvsum 11021 inffinp1 11787 unct 11797 isbasis2g 12055 tgval2 12063 ntreq0 12144 lmff 12260 metrest 12495 bj-axempty 12783 bj-axempty2 12784 bj-vprc 12786 bdinex1 12789 bj-zfpair2 12800 bj-uniex2 12806 bj-d0clsepcl 12815 |
Copyright terms: Public domain | W3C validator |