MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbii Structured version   Visualization version   GIF version

Theorem exbii 1851
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1 (𝜑𝜓)
Assertion
Ref Expression
exbii (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1850 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1800 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  2exbii  1852  3exbii  1853  exanali  1863  exancom  1865  19.43  1886  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistr  1959  exdistr2  1963  3exdistr  1965  19.12vvv  1993  excom13  2165  exrot4  2167  2sb5  2272  dfsb7  2276  eeor  2330  eeorOLD  2331  19.12vv  2344  eean  2345  eeeanv  2347  ee4anv  2348  2sb8ef  2353  equsexALT  2418  2sb5rf  2471  2sb8e  2534  mo4  2565  eu6lem  2572  eubii  2584  sb8eulem  2597  cbvmovw  2601  cbvmow  2602  eu1  2611  sbmo  2615  2moswapv  2630  2moswap  2645  euae  2660  issetlem  2818  clabel  2886  sbabel  2942  sbabelOLD  2943  nabbi  3048  rextru  3081  rexbii2  3094  r2exlem  3141  r19.41v  3186  r19.41  3249  rexcom4  3274  rexcomOLD  3277  2ex2rexrot  3284  rexv  3473  cgsex4g  3493  cgsex4gOLD  3494  ceqsex2  3501  ceqsex2v  3502  ceqsex3v  3503  gencbvex  3507  spc3egv  3565  spc3gv  3566  ceqsrexv  3610  rexabOLD  3658  rexrab2  3663  euxfrw  3684  euxfr  3686  euind  3687  reu6  3689  reu3  3690  2reuswap  3709  2reuswap2  3710  reuind  3716  2reu5lem3  3720  2reu5  3721  2rmoswap  3724  sbcimdv  3818  sbcg  3823  sbccomlem  3831  rmo2  3848  rmoanim  3855  rmoanimALT  3856  rexun  4155  reupick3  4284  euelss  4286  ndisj  4332  abn0OLD  4346  pssnel  4435  rexsns  4635  exsnrex  4646  snprc  4683  euabsn2  4691  reusn  4693  eusn  4696  elpreqpr  4829  elunirab  4886  uniprg  4887  uniprOLD  4889  uniun  4896  uniin  4897  uni0b  4899  uniintsn  4953  iuncom4  4967  dfiun2g  4995  dfiun2gOLD  4996  iunn0  5032  iunxiun  5062  disjor  5090  cbvopab2  5187  cbvopab2v  5191  unopab  5192  axrep1  5248  axrep4  5252  axrep5  5253  axrep6  5254  zfrep4  5258  axsepgfromrep  5259  axnulALT  5266  0ex  5269  vnex  5276  inex1  5279  inuni  5305  axpweq  5310  zfpow  5326  axpow2  5327  axpow3  5328  vpwex  5337  zfpair  5381  zfpair2  5390  el  5399  eqvinop  5449  copsexgw  5452  copsexg  5453  opabn0  5515  iunopab  5521  iunopabOLD  5522  dfid2  5538  dfid3  5539  opeliunxp  5704  xpiundi  5707  xpiundir  5708  elvvv  5712  csbxp  5736  eliunxp  5798  exopxfr  5804  relop  5811  opelco2g  5828  cnvco  5846  cnvuni  5847  dfdm3  5848  dfrn2  5849  dfrn3  5850  elrng  5852  dfdm4  5856  csbdm  5858  eldm2g  5860  dmun  5871  dmin  5872  dmiun  5874  dmuni  5875  dmopab  5876  dmi  5882  dmep  5884  rnep  5887  rnopab  5914  dmcosseq  5933  dmres  5964  elsnres  5982  dfima2  6020  elima3  6025  imadmrn  6028  imai  6031  args  6049  rniun  6105  xpdifid  6125  ssrnres  6135  dmsnn0  6164  dmsnopg  6170  cnvresima  6187  mptpreima  6195  dfco2  6202  coundi  6204  coundir  6205  resco  6207  imaco  6208  rnco  6209  coiun  6213  coi1  6219  coass  6222  xpco  6246  elsnxp  6248  dfpo2  6253  dffun2OLDOLD  6513  dffun5  6518  imadif  6590  funimaexgOLD  6593  brprcneu  6837  brprcneuALT  6838  dffv2  6941  fndmin  7000  fvn0ssdmfun  7030  abrexco  7196  imaiun  7197  isomin  7287  imaeqsexv  7313  dfoprab2  7420  cbvoprab2  7450  zfun  7678  uniex2  7680  uniuni  7701  elxp4  7864  elxp5  7865  fiun  7880  f1iun  7881  f11o  7884  fvresex  7897  opabex3d  7903  opabex3rd  7904  opabex3  7905  abexssex  7908  abexex  7909  oprabrexex2  7916  releldm2  7980  dfopab2  7989  dfoprab3s  7990  fsplit  8054  frxp  8063  suppvalbr  8101  cnvimadfsn  8108  brtpos2  8168  dfwrecsOLD  8249  wfrfunOLD  8270  dfrecs3  8323  dfrecs3OLD  8324  oarec  8514  oeeu  8555  domen  8908  xpsnen  9006  xpcomco  9013  xpassen  9017  dif1enOLD  9113  inf2  9566  zfinf  9582  axinf2  9583  zfinf2  9585  brttrcl2  9657  ttrcltr  9659  ttrclresv  9660  ttrclselem2  9669  rankuni  9806  scott0  9829  cp  9834  ween  9978  aceq1  10060  aceq0  10061  aceq2  10062  dfac5lem1  10066  dfac5lem2  10067  dfac5lem3  10068  kmlem3  10095  kmlem14  10106  kmlem15  10107  kmlem16  10108  cflem  10189  cf0  10194  cfval2  10203  cfss  10208  cfslb  10209  fin23lem32  10287  axdc2lem  10391  zfac  10403  ac9  10426  ac9s  10436  axpowndlem3  10542  zfcndrep  10557  zfcndun  10558  zfcndpow  10559  zfcndinf  10561  zfcndac  10562  axgroth5  10767  axgroth2  10768  axgroth6  10771  axgroth3  10774  axgroth4  10775  grothprim  10777  grothtsk  10778  genpass  10952  ltexprlem1  10979  ltexprlem4  10982  supaddc  12129  supadd  12130  supmul1  12131  supmullem2  12133  2rexuz  12832  nnwos  12847  hashgt23el  14331  hashfun  14344  wwlktovfo  14854  xpcogend  14866  cbvsum  15587  cbvprod  15805  iprodmul  15893  maxprmfct  16592  4sqlem12  16835  vdwmc  16857  cshwrepswhash1  16982  imasleval  17430  isacs2  17540  cicsym  17694  gsumval3eu  19688  lidlnz  20714  isbasis2g  22314  tgval2  22322  ntreq0  22444  lmff  22668  cmpfi  22775  is1stc2  22809  1stcelcls  22828  unisngl  22894  isfbas2  23202  elfg  23238  alexsubALTlem3  23416  ustfilxp  23580  metrest  23896  metuel2  23937  restmetu  23942  dchrvmasumlema  26864  elold  27221  lrrecfr  27277  sleadd1  27320  addsunif  27332  addsasslem1  27333  addsasslem2  27334  istrkg2ld  27444  istrkg3ld  27445  1loopgrvd2  28493  wwlksnextsurj  28887  isgrpo  29481  nmo  31460  reuxfrdf  31461  rexunirn  31462  dmrab  31467  disjorf  31539  fcoinvbr  31568  mpomptxf  31639  cnvoprabOLD  31679  fpwrelmapffslem  31691  ordtconnlem1  32545  ddemeas  32875  omssubaddlem  32939  omssubadd  32940  eulerpartlemgvv  33016  bnj89  33373  bnj133  33379  bnj1019  33431  bnj1101  33436  bnj1109  33438  bnj1143  33442  bnj1198  33447  bnj1304  33471  bnj605  33559  bnj607  33568  bnj600  33571  bnj865  33575  bnj916  33585  bnj983  33603  bnj985v  33605  bnj985  33606  bnj996  33608  bnj1033  33621  bnj1083  33630  bnj1090  33631  bnj1093  33632  bnj1110  33634  bnj1128  33642  bnj1145  33645  bnj1171  33652  bnj1172  33653  bnj1174  33655  bnj1176  33657  bnj1186  33659  bnj1189  33661  bnj1253  33669  bnj1279  33670  bnj1371  33681  bnj1374  33683  bnj1312  33710  exdifsn  33725  fineqvrep  33736  fineqvpow  33737  lfuhgr3  33753  loop1cycl  33771  satfvsucsuc  33999  satf0op  34011  axextprim  34312  axrepprim  34313  axunprim  34314  axpowprim  34315  axregprim  34316  axinfprim  34317  axacprim  34318  dftr6  34363  coep  34364  coepr  34365  dffr5  34366  cnvco1  34371  cnvco2  34372  eldm3  34373  fundmpss  34380  dfdm5  34386  dfrn5  34387  elima4  34389  axextdfeq  34411  19.12b  34415  axextndbi  34418  brtxp  34494  brpprod  34499  brsset  34503  dfon3  34506  brtxpsd  34508  elfix  34517  dffix2  34519  sscoid  34527  dffun10  34528  elfuns  34529  elsingles  34532  snelsingles  34536  dfiota3  34537  brimg  34551  brapply  34552  brcup  34553  brcap  34554  brsuccf  34555  funpartlem  34556  brrestrict  34563  dfrecs2  34564  dfrdg4  34565  neifg  34872  bj-equsexval  35153  bj-eeanvw  35207  bj-substw  35216  eliminable-abelv  35364  eliminable-abelab  35365  bj-denoteslem  35366  bj-rexvw  35376  bj-csbsnlem  35399  bj-gabima  35439  bj-snsetex  35463  bj-elsngl  35468  bj-snglc  35469  bj-abex  35530  bj-clex  35531  bj-clel3gALT  35548  bj-nul  35556  bj-dfid2ALT  35565  bj-restpw  35592  bj-restuni  35597  bj-dfmpoa  35618  bj-opabco  35688  bj-xpcossxp  35689  bj-imdirco  35690  mptsnunlem  35838  topdifinffinlem  35847  difunieq  35874  wl-dfclab  36077  poimirlem26  36133  ismblfin  36148  itg2addnclem3  36160  itg2addnc  36161  ismgmOLD  36338  sbcexfi  36605  sbccom2lem  36612  eldmres  36759  ecinn0  36843  ineleq  36844  moantr  36854  rnxrn  36889  rnxrnres  36890  dfcoss2  36904  dfcoss3  36905  cosscnv  36907  coss1cnvres  36908  coss2cnvepres  36909  1cossres  36920  cocossss  36927  rncossdmcoss  36946  eldmcoss2  36950  coss0  36970  cossid  36971  dfssr2  36990  eldmqs1cossres  37150  prtlem16  37360  prter2  37372  islshpat  37508  islpln5  38027  islvol5  38071  pmapglb  38262  polval2N  38398  cdlemftr3  39057  dibelval3  39639  dicelval3  39672  dihglb2  39834  sn-axrep5v  40667  prjspeclsp  40979  diophrex  41127  onsupmaxb  41602  nnoeomeqom  41676  rp-isfinite6  41864  snen1g  41870  relintab  41929  imaiun1  41997  coiun1  41998  clsk3nimkb  42386  expandexn  42643  ismnuprim  42648  rr-groth  42653  ismnushort  42655  rr-grothshortbi  42657  19.36vv  42737  19.37vv  42739  pm11.58  42744  pm11.6  42746  pm13.192  42764  2sbc5g  42770  iotasbc2  42774  onfrALTlem5  42898  onfrALTlem1  42904  ax6e2nd  42914  2sb5nd  42916  en3lplem2VD  43200  onfrALTlem5VD  43241  relopabVD  43257  ax6e2ndVD  43264  2sb5ndVD  43266  ax6e2ndALT  43286  2sb5ndALT  43288  rfcnnnub  43315  inn0f  43355  stoweidlem34  44349  stoweidlem35  44350  stoweidlem60  44375  smfpimcc  45123  ichexmpl1  45735  sprid  45740  opeliun2xp  46482  eliunxp2  46483  mosssn2  46975  setrec1lem3  47208  elpglem3  47232  eximp-surprise  47305
  Copyright terms: Public domain W3C validator