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

Theorem exbii 1849
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 1848 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1799 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  2exbii  1850  3exbii  1851  exanali  1860  exancom  1862  19.43  1883  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistr  1955  exdistr2  1959  19.42vvvOLD  1961  3exdistr  1962  19.12vvv  1995  equsexvwOLD  2012  excom13  2169  exrot4  2171  equsexv  2268  2sb5  2280  dfsb7  2283  dfsb7OLD  2284  eeor  2346  19.12vv  2360  eean  2361  eeeanv  2363  ee4anv  2364  2sb8ev  2367  equsexALT  2433  2sb5rf  2488  2sb8e  2555  mo4  2628  eu6lem  2636  eubii  2648  sb8eulem  2662  cbvmow  2666  eu1  2674  sbmo  2678  2moswapv  2694  2moswap  2709  euae  2725  clabel  2937  sbabel  2989  nabbi  3092  rexbii2  3211  rexcom4  3215  2ex2rexrot  3216  r2exlem  3264  r19.41v  3303  r19.41  3304  rexcom  3311  isset  3456  rexv  3470  cgsex4g  3489  cgsex4gOLD  3490  ceqsex2  3494  ceqsex2v  3495  ceqsex3v  3496  gencbvex  3500  vtocl2OLD  3513  spc3egv  3555  spc3gv  3556  ceqsrexv  3600  rexab  3637  rexrab2  3644  euxfrw  3663  euxfr  3665  euind  3666  reu6  3668  reu3  3669  2reuswap  3688  2reuswap2  3689  reuind  3695  2reu5lem3  3699  2reu5  3700  2rmoswap  3703  sbccomlem  3802  rmo2  3819  rmoanim  3826  rmoanimALT  3827  rexun  4120  reupick3  4243  euelss  4245  ndisj  4284  abn0  4293  pssnel  4381  rexsns  4572  exsnrex  4581  snprc  4616  euabsn2  4624  reusn  4626  eusn  4629  elpreqpr  4760  elunirab  4819  unipr  4820  uniun  4826  uniin  4827  uni0b  4829  uniintsn  4878  iuncom4  4892  dfiun2g  4920  dfiun2gOLD  4921  iunn0  4955  iunxiun  4985  disjor  5013  cbvopab2  5108  cbvopab2v  5111  unopab  5112  axrep1  5158  axrep4  5162  axrep5  5163  axrep6  5164  zfrep4  5167  axsepgfromrep  5168  axnulALT  5175  0ex  5178  vnex  5185  inex1  5188  inuni  5213  axpweq  5233  zfpow  5235  axpow2  5236  axpow3  5237  vpwex  5246  zfpair  5290  zfpair2  5299  eqvinop  5346  copsexgw  5349  copsexg  5350  opabn0  5408  iunopab  5414  dfid3  5430  opeliunxp  5587  xpiundi  5590  xpiundir  5591  elvvv  5595  csbxp  5618  eliunxp  5676  exopxfr  5682  relop  5689  opelco2g  5706  cnvco  5724  cnvuni  5725  dfdm3  5726  dfrn2  5727  dfrn3  5728  elrng  5730  dfdm4  5732  csbdm  5734  eldm2g  5736  dmun  5747  dmin  5748  dmiun  5750  dmuni  5751  dmopab  5752  dmi  5759  dmep  5761  domepOLD  5762  rnep  5765  elrn  5790  rnopab  5794  dmcosseq  5813  dmres  5844  elsnres  5862  dfima2  5902  elima3  5907  imadmrn  5910  imai  5913  args  5928  rniun  5977  xpdifid  5996  ssrnres  6006  dmsnn0  6035  dmsnopg  6041  cnvresima  6058  mptpreima  6063  dfco2  6069  coundi  6071  coundir  6072  resco  6074  imaco  6075  rnco  6076  coiun  6080  coi1  6086  coass  6089  xpco  6112  elsnxp  6114  dffun2  6338  dffun5  6341  imadif  6412  funimaexg  6414  brprcneu  6641  dffv2  6737  fndmin  6796  fvn0ssdmfun  6823  abrexco  6985  imaiun  6986  isomin  7073  dfoprab2  7195  cbvoprab2  7225  zfun  7446  uniex2  7448  uniuni  7468  elxp4  7613  elxp5  7614  fiun  7630  f1iun  7631  f11o  7634  fvresex  7647  opabex3d  7652  opabex3rd  7653  opabex3  7654  abexssex  7657  abexex  7658  oprabrexex2  7665  releldm2  7728  dfopab2  7736  dfoprab3s  7737  fsplit  7799  fsplitOLD  7800  frxp  7807  suppvalbr  7821  cnvimadfsn  7826  brtpos2  7885  wfrfun  7952  dfrecs3  7996  oarec  8175  oeeu  8216  domen  8509  xpsnen  8588  xpcomco  8594  xpassen  8598  inf2  9074  zfinf  9090  axinf2  9091  zfinf2  9093  rankuni  9280  scott0  9303  cp  9308  ween  9450  aceq1  9532  aceq0  9533  aceq2  9534  dfac5lem1  9538  dfac5lem2  9539  dfac5lem3  9540  kmlem3  9567  kmlem14  9578  kmlem15  9579  kmlem16  9580  cflem  9661  cf0  9666  cfval2  9675  cfss  9680  cfslb  9681  fin23lem32  9759  axdc2lem  9863  zfac  9875  ac9  9898  ac9s  9908  axpowndlem3  10014  zfcndrep  10029  zfcndun  10030  zfcndpow  10031  zfcndinf  10033  zfcndac  10034  axgroth5  10239  axgroth2  10240  axgroth6  10243  axgroth3  10246  axgroth4  10247  grothprim  10249  grothtsk  10250  genpass  10424  ltexprlem1  10451  ltexprlem4  10454  supaddc  11599  supadd  11600  supmul1  11601  supmullem2  11603  2rexuz  12292  nnwos  12307  hashgt23el  13785  hashfun  13798  wwlktovfo  14317  xpcogend  14329  cbvsum  15047  cbvprod  15264  iprodmul  15352  maxprmfct  16046  4sqlem12  16285  vdwmc  16307  cshwrepswhash1  16431  imasleval  16809  isacs2  16919  cicsym  17069  gsumval3eu  19020  lidlnz  19997  isbasis2g  21556  tgval2  21564  ntreq0  21685  lmff  21909  cmpfi  22016  is1stc2  22050  1stcelcls  22069  unisngl  22135  isfbas2  22443  elfg  22479  alexsubALTlem3  22657  ustfilxp  22821  metrest  23134  metuel2  23175  restmetu  23180  dchrvmasumlema  26087  istrkg2ld  26257  istrkg3ld  26258  1loopgrvd2  27296  wwlksnextsurj  27689  isgrpo  28283  nmo  30264  reuxfrdf  30265  rexunirn  30266  dmrab  30270  disjorf  30345  fcoinvbr  30374  mpomptxf  30445  cnvoprabOLD  30485  fpwrelmapffslem  30497  ordtconnlem1  31275  ddemeas  31603  omssubaddlem  31665  omssubadd  31666  eulerpartlemgvv  31742  bnj89  32099  bnj133  32105  bnj1019  32159  bnj1101  32164  bnj1109  32166  bnj1143  32170  bnj1198  32175  bnj1304  32199  bnj605  32287  bnj607  32296  bnj600  32299  bnj865  32303  bnj916  32313  bnj983  32331  bnj985v  32333  bnj985  32334  bnj996  32336  bnj1033  32349  bnj1083  32358  bnj1090  32359  bnj1093  32360  bnj1110  32362  bnj1128  32370  bnj1145  32373  bnj1171  32380  bnj1172  32381  bnj1174  32383  bnj1176  32385  bnj1186  32387  bnj1189  32389  bnj1253  32397  bnj1279  32398  bnj1371  32409  bnj1374  32411  bnj1312  32438  exdifsn  32453  lfuhgr3  32474  loop1cycl  32492  satfvsucsuc  32720  satf0op  32732  axextprim  33035  axrepprim  33036  axunprim  33037  axpowprim  33038  axregprim  33039  axinfprim  33040  axacprim  33041  dftr6  33094  coep  33095  coepr  33096  dffr5  33097  dfpo2  33099  cnvco1  33103  cnvco2  33104  eldm3  33105  fundmpss  33117  dfdm5  33124  dfrn5  33125  elima4  33127  axextdfeq  33150  19.12b  33154  axextndbi  33157  brtxp  33449  brpprod  33454  brsset  33458  dfon3  33461  brtxpsd  33463  elfix  33472  dffix2  33474  sscoid  33482  dffun10  33483  elfuns  33484  elsingles  33487  snelsingles  33491  dfiota3  33492  brimg  33506  brapply  33507  brcup  33508  brcap  33509  brsuccf  33510  funpartlem  33511  brrestrict  33518  dfrecs2  33519  dfrdg4  33520  neifg  33827  bj-equsexval  34101  bj-eeanvw  34155  bj-substw  34164  eliminable-abelv  34302  eliminable-abelab  34303  bj-denoteslem  34304  bj-rexvw  34315  bj-csbsnlem  34339  bj-snsetex  34394  bj-elsngl  34399  bj-snglc  34400  bj-nul  34468  bj-restpw  34502  bj-restuni  34507  bj-dfmpoa  34528  bj-opabco  34598  bj-xpcossxp  34599  bj-imdirco  34600  mptsnunlem  34750  topdifinffinlem  34759  difunieq  34786  wl-dfclab  34986  wl-dfrmosb  35011  wl-dfrmov  35012  poimirlem26  35076  ismblfin  35091  itg2addnclem3  35103  itg2addnc  35104  ismgmOLD  35281  sbcexfi  35548  sbccom2lem  35555  eldmres  35683  ecinn0  35760  ineleq  35761  moantr  35769  rnxrn  35799  rnxrnres  35800  dfcoss2  35814  dfcoss3  35815  1cossres  35827  cocossss  35834  rncossdmcoss  35848  eldmcoss2  35852  coss0  35872  cossid  35873  dfssr2  35892  eldmqs1cossres  36046  prtlem16  36158  prter2  36170  islshpat  36306  islpln5  36824  islvol5  36868  pmapglb  37059  polval2N  37195  cdlemftr3  37854  dibelval3  38436  dicelval3  38469  dihglb2  38631  sn-axrep5v  39387  prjspeclsp  39593  diophrex  39703  rp-isfinite6  40213  snen1g  40219  relintab  40270  imaiun1  40339  coiun1  40340  clsk3nimkb  40730  expandexn  40984  ismnuprim  40989  rr-groth  40994  19.36vv  41074  19.37vv  41076  pm11.58  41081  pm11.6  41083  pm13.192  41101  2sbc5g  41107  iotasbc2  41111  onfrALTlem5  41235  onfrALTlem1  41241  ax6e2nd  41251  2sb5nd  41253  en3lplem2VD  41537  onfrALTlem5VD  41578  relopabVD  41594  ax6e2ndVD  41601  2sb5ndVD  41603  ax6e2ndALT  41623  2sb5ndALT  41625  rfcnnnub  41652  inn0f  41694  stoweidlem34  42663  stoweidlem35  42664  stoweidlem60  42689  smfpimcc  43426  ichexmpl1  43973  sprid  43978  opeliun2xp  44721  eliunxp2  44722  setrec1lem3  45206  elpglem3  45229  eximp-surprise  45299
  Copyright terms: Public domain W3C validator