![]() |
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 | ⊢ (∃xφ ↔ ∃xψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbi 1492 | . 2 ⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ)) | |
2 | exbii.1 | . 2 ⊢ (φ ↔ ψ) | |
3 | 1, 2 | mpg 1337 | 1 ⊢ (∃xφ ↔ ∃xψ) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∃wex 1378 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 2exbii 1494 3exbii 1495 exancom 1496 excom13 1576 exrot4 1578 eeor 1582 sbcof2 1688 sbequ8 1724 sbidm 1728 sborv 1767 19.41vv 1780 19.41vvv 1781 19.41vvvv 1782 exdistr 1784 19.42vvv 1786 exdistr2 1788 3exdistr 1789 4exdistr 1790 eean 1803 eeeanv 1805 ee4anv 1806 2sb5 1856 2sb5rf 1862 sbel2x 1871 sbexyz 1876 sbex 1877 exsb 1881 2exsb 1882 sb8eu 1910 sb8euh 1920 eu1 1922 eu2 1941 2moswapdc 1987 2exeu 1989 exists1 1993 clelab 2159 clabel 2160 sbabel 2200 rexbii2 2329 r2exf 2336 nfrexdya 2353 r19.41 2459 r19.43 2462 isset 2555 rexv 2566 ceqsex2 2588 ceqsex3v 2590 gencbvex 2594 ceqsrexv 2668 rexab 2697 rexrab2 2702 euxfrdc 2721 euind 2722 reu6 2724 reu3 2725 2reuswapdc 2737 reuind 2738 sbccomlem 2826 rmo2ilem 2841 rexun 3117 reupick3 3216 abn0r 3237 rabn0m 3239 rexsns 3400 rexsnsOLD 3401 exsnrex 3404 snprc 3426 euabsn2 3430 reusn 3432 eusn 3435 elunirab 3584 unipr 3585 uniun 3590 uniin 3591 iuncom4 3655 dfiun2g 3680 iunn0m 3708 iunxiun 3727 cbvopab2 3822 cbvopab2v 3825 unopab 3827 zfnuleu 3872 0ex 3875 vprc 3879 inex1 3882 intexabim 3897 iinexgm 3899 inuni 3900 unidif0 3911 axpweq 3915 zfpow 3919 axpow2 3920 axpow3 3921 pwex 3923 zfpair2 3936 mss 3953 exss 3954 opm 3962 eqvinop 3971 copsexg 3972 opabm 4008 iunopab 4009 zfun 4137 uniex2 4139 uniuni 4149 rexxfrd 4161 dtruex 4237 zfinf2 4255 elxp2 4306 opeliunxp 4338 xpiundi 4341 xpiundir 4342 elvvv 4346 eliunxp 4418 rexiunxp 4421 relop 4429 opelco2g 4446 cnvco 4463 cnvuni 4464 dfdm3 4465 dfrn2 4466 dfrn3 4467 elrng 4469 dfdm4 4470 eldm2g 4474 dmun 4485 dmin 4486 dmiun 4487 dmuni 4488 dmopab 4489 dmi 4493 dmmrnm 4497 elrn 4520 rnopab 4524 dmcosseq 4546 dmres 4575 elres 4589 elsnres 4590 dfima2 4613 elima3 4618 imadmrn 4621 imai 4624 args 4637 rniun 4677 ssrnres 4706 dmsnm 4729 dmsnopg 4735 elxp4 4751 elxp5 4752 cnvresima 4753 mptpreima 4757 dfco2 4763 coundi 4765 coundir 4766 resco 4768 imaco 4769 rnco 4770 coiun 4773 coi1 4779 coass 4782 xpcom 4807 dffun2 4855 imadif 4922 imainlem 4923 funimaexglem 4925 fun11iun 5090 f11o 5102 brprcneu 5114 nfvres 5149 fndmin 5217 abrexco 5341 imaiun 5342 dfoprab2 5494 cbvoprab2 5519 rexrnmpt2 5558 opabex3d 5690 opabex3 5691 abexssex 5694 abexex 5695 oprabrexex2 5699 releldm2 5753 dfopab2 5757 dfoprab3s 5758 brtpos2 5807 domen 6168 xpsnen 6231 xpcomco 6236 xpassen 6240 subhalfnqq 6397 ltbtwnnq 6399 prnmaxl 6471 prnminu 6472 prarloc 6486 genpdflem 6490 genpassl 6507 genpassu 6508 ltexprlemm 6574 2rexuz 8301 bj-axempty 9348 bj-axempty2 9349 bj-vprc 9351 bdinex1 9354 bj-zfpair2 9365 bj-uniex2 9371 bj-d0clsepcl 9384 |
Copyright terms: Public domain | W3C validator |