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 1583 | . 2 | |
2 | exbii.1 | . 2 | |
3 | 1, 2 | mpg 1427 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2exbii 1585 3exbii 1586 exancom 1587 excom13 1667 exrot4 1669 eeor 1673 sbcof2 1782 sbequ8 1819 sbidm 1823 sborv 1862 19.41vv 1875 19.41vvv 1876 19.41vvvv 1877 exdistr 1881 19.42vvv 1884 exdistr2 1886 3exdistr 1887 4exdistr 1888 eean 1903 eeeanv 1905 ee4anv 1906 2sb5 1958 2sb5rf 1964 sbel2x 1973 sbexyz 1978 sbex 1979 exsb 1983 2exsb 1984 sb8eu 2012 sb8euh 2022 eu1 2024 eu2 2043 2moswapdc 2089 2exeu 2091 exists1 2095 clelab 2265 clabel 2266 sbabel 2307 rexbii2 2446 r2exf 2453 nfrexdya 2470 r19.41 2586 r19.43 2589 isset 2692 rexv 2704 ceqsex2 2726 ceqsex3v 2728 gencbvex 2732 ceqsrexv 2815 rexab 2846 rexrab2 2851 euxfrdc 2870 euind 2871 reu6 2873 reu3 2874 2reuswapdc 2888 reuind 2889 sbccomlem 2983 rmo2ilem 2998 rexun 3256 reupick3 3361 abn0r 3387 abn0m 3388 rabn0m 3390 rexsns 3563 exsnrex 3566 snprc 3588 euabsn2 3592 reusn 3594 eusn 3597 elunirab 3749 unipr 3750 uniun 3755 uniin 3756 iuncom4 3820 dfiun2g 3845 iunn0m 3873 iunxiun 3894 disjnim 3920 cbvopab2 4002 cbvopab2v 4005 unopab 4007 zfnuleu 4052 0ex 4055 vnex 4059 inex1 4062 intexabim 4077 iinexgm 4079 inuni 4080 unidif0 4091 axpweq 4095 zfpow 4099 axpow2 4100 axpow3 4101 vpwex 4103 zfpair2 4132 mss 4148 exss 4149 opm 4156 eqvinop 4165 copsexg 4166 opabm 4202 iunopab 4203 zfun 4356 uniex2 4358 uniuni 4372 rexxfrd 4384 dtruex 4474 zfinf2 4503 elxp2 4557 opeliunxp 4594 xpiundi 4597 xpiundir 4598 elvvv 4602 eliunxp 4678 rexiunxp 4681 relop 4689 elco 4705 opelco2g 4707 cnvco 4724 cnvuni 4725 dfdm3 4726 dfrn2 4727 dfrn3 4728 elrng 4730 dfdm4 4731 eldm2g 4735 dmun 4746 dmin 4747 dmiun 4748 dmuni 4749 dmopab 4750 dmi 4754 dmmrnm 4758 elrn 4782 rnopab 4786 dmcosseq 4810 dmres 4840 elres 4855 elsnres 4856 dfima2 4883 elima3 4888 imadmrn 4891 imai 4895 args 4908 rniun 4949 ssrnres 4981 dmsnm 5004 dmsnopg 5010 elxp4 5026 elxp5 5027 cnvresima 5028 mptpreima 5032 dfco2 5038 coundi 5040 coundir 5041 resco 5043 imaco 5044 rnco 5045 coiun 5048 coi1 5054 coass 5057 xpcom 5085 dffun2 5133 imadif 5203 imainlem 5204 funimaexglem 5206 fun11iun 5388 f11o 5400 brprcneu 5414 nfvres 5454 fndmin 5527 abrexco 5660 imaiun 5661 dfoprab2 5818 cbvoprab2 5844 rexrnmpo 5886 opabex3d 6019 opabex3 6020 abexssex 6023 abexex 6024 oprabrexex2 6028 releldm2 6083 dfopab2 6087 dfoprab3s 6088 cnvoprab 6131 brtpos2 6148 tfr1onlemaccex 6245 tfrcllembxssdm 6253 tfrcllemaccex 6258 domen 6645 mapsnen 6705 xpsnen 6715 xpcomco 6720 xpassen 6724 fimax2gtri 6795 supelti 6889 subhalfnqq 7222 ltbtwnnq 7224 prnmaxl 7296 prnminu 7297 prarloc 7311 genpdflem 7315 genpassl 7332 genpassu 7333 ltexprlemm 7408 2rexuz 9377 seq3f1olemp 10275 cbvsum 11129 cbvprod 11327 inffinp1 11942 unct 11954 isbasis2g 12212 tgval2 12220 ntreq0 12301 lmff 12418 metrest 12675 bj-axempty 13091 bj-axempty2 13092 bj-vprc 13094 bdinex1 13097 bj-zfpair2 13108 bj-uniex2 13114 bj-d0clsepcl 13123 |
Copyright terms: Public domain | W3C validator |