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

Theorem rexbii 3210
 Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Dec-2019.)
Hypothesis
Ref Expression
rexbii.1 (𝜑𝜓)
Assertion
Ref Expression
rexbii (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)

Proof of Theorem rexbii
StepHypRef Expression
1 rexbii.1 . . 3 (𝜑𝜓)
21anbi2i 625 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3208 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2111  ∃wrex 3107 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-an 400  df-ex 1782  df-rex 3112 This theorem is referenced by:  2rexbii  3211  2ex2rexrot  3213  rexcom4a  3214  r19.29imd  3218  rexnal2  3219  r19.41vv  3302  r19.42v  3303  r19.43  3304  rexcom  3308  rexcom13  3313  rexrot4  3315  3reeanv  3321  2ralor  3322  cbvrex2vw  3409  cbvrex2v  3412  rexcom4b  3471  rexcom4OLD  3473  ceqsrex2v  3599  clel5  3605  reu7  3671  2reu5a  3683  0el  4274  n0snor2el  4724  uni0b  4826  iuncom  4888  iuncom4  4889  iuniin  4893  dfiunv2  4922  iunab  4938  iunn0  4952  iunin2  4956  iundif2  4959  iunun  4978  iunxiun  4982  iunpwss  4992  axrep6  5161  inuni  5210  reusv2lem5  5268  iunopab  5411  dffr2  5484  frc  5485  frminex  5499  dfepfr  5504  epfrc  5505  xpiundi  5586  xpiundir  5587  reliin  5654  iunxpf  5683  cnvuni  5721  dmiun  5746  dmopab2rex  5750  elres  5857  elidinxp  5878  dfima3  5899  dffr3  5929  rniun  5973  xpdifid  5992  dminxp  6004  imaco  6071  coiun  6076  dffr4  6132  tz6.26  6147  sucel  6232  isarep1  6412  rexrn  6830  ralrn  6831  elrnrexdmb  6833  fnasrn  6884  rexima  6977  ralima  6978  abrexco  6981  imaiun  6982  fliftcnv  7043  rexrnmpo  7270  iunpw  7475  abrexex2g  7649  el2xptp  7719  rdglem1  8036  tz7.49  8066  oarec  8173  omeu  8196  qsid  8348  eroveu  8377  ixp0  8480  fimax2g  8750  marypha2lem2  8886  dfsup2  8894  infcllem  8937  dfoi  8961  wemapsolem  9000  zfregcl  9044  zfreg  9045  zfregfr  9054  oemapso  9131  zfregs2  9161  infenaleph  9504  isinfcard  9505  kmlem7  9569  kmlem13  9575  fin23lem26  9738  dffin1-5  9801  fin12  9826  numth  9885  ac6n  9898  zorn2lem7  9915  zorng  9917  brdom7disj  9944  brdom6disj  9945  uniwun  10153  axgroth5  10237  axgroth4  10245  grothprim  10247  npomex  10409  genpass  10422  elreal  10544  dfinfre  11611  infrenegsup  11613  uzwo  12301  ublbneg  12323  xrinfmss2  12694  4fvwrd4  13024  fsuppmapnn0fiubex  13357  fsuppmapnn0ub  13360  mptnn0fsuppr  13364  hashge2el2dif  13836  dfrtrclrec2  14411  rexanuz  14699  rexfiuz  14701  clim0  14857  cbvsum  15046  incexc2  15187  cbvprod  15263  fprodle  15344  iprodmul  15351  divalglem10  15745  divalgb  15747  ncoprmlnprm  16060  pythagtriplem2  16146  pythagtriplem19  16162  pythagtrip  16163  pceu  16175  prmreclem6  16249  4sqlem12  16284  cshwshashlem1  16423  cshwshash  16432  imasaddfnlem  16795  isdrs2  17543  smndex1mgm  18066  smndex1n0mnd  18071  pmtrprfvalrn  18611  pgpfac1lem5  19197  dvdsrval  19394  opprunit  19410  lsmspsn  19852  lsmelval2  19853  islpidl  20015  mat1dimelbas  21083  mat1dimbas  21084  mdetunilem8  21231  pmatcollpw2lem  21389  tgval2  21568  ntreq0  21689  isclo2  21700  neiptopnei  21744  ist0-3  21957  tgcmp  22013  cmpfi  22020  is1stc2  22054  unisngl  22139  xkobval  22198  txtube  22252  txcmplem1  22253  xkococnlem  22271  eltsms  22745  metrest  23138  iscau3  23889  bcth  23940  pmltpc  24061  itg2i1fseq  24366  itg2cn  24374  plyun0  24801  aaliou3lem9  24953  1cubr  25435  dchrvmasumlema  26091  selbergsb  26166  ostth  26230  istrkg2ld  26261  tglowdim1i  26302  legtrid  26392  midex  26538  ishpg  26560  brbtwn2  26706  colinearalg  26711  ax5seg  26739  axpasch  26742  axlowdimlem6  26748  axeuclidlem  26763  axeuclid  26764  elntg2  26786  umgr2edg1  27008  umgr2edgneu  27011  nbgrsym  27160  isuvtx  27192  usgr2pth0  27561  wlkiswwlksupgr2  27670  clwwlknun  27904  4cycl2vnunb  28082  fusgreg2wsp  28128  lpni  28270  nmobndseqi  28569  hhcmpl  28990  shne0i  29238  nmcopexi  29817  nmcfnexi  29841  cdj3lem3b  30230  rexcom4f  30248  reuxfrdf  30269  iunin1f  30328  ofpreima  30435  intimafv  30477  fpwrelmapffslem  30501  tosglblem  30689  xrnarchi  30870  lsmsnorb  31006  ordtconnlem1  31289  lmdvg  31318  esumfsup  31451  reprsuc  32008  reprdifc  32020  bnj168  32122  bnj1185  32187  bnj1542  32251  bnj865  32317  bnj916  32327  bnj983  32345  bnj1176  32399  bnj1189  32403  bnj1296  32415  bnj1398  32428  bnj1450  32444  bnj1463  32449  nummin  32486  loop1cycl  32509  cvmliftlem15  32670  cvmlift2lem12  32686  satfvsuclem2  32732  satfvsucsuc  32737  satfdm  32741  satf0  32744  dmopab3rexdif  32777  dffr5  33114  imaindm  33147  dfon2lem9  33161  frpomin2  33204  soseq  33221  frrlem9  33256  noseponlem  33296  nosepon  33297  nolt02o  33324  brbigcup  33484  elfuns  33501  brimage  33512  brimg  33523  dfrecs2  33536  imagesset  33539  brub  33540  brsegle  33694  filnetlem4  33854  bj-rexcom4bv  34338  bj-rexcom4b  34339  bj-elsngl  34420  bj-rest10  34519  bj-restreg  34530  bj-mpomptALT  34550  nlpineqsn  34841  fvineqsneq  34845  iundif1  35047  matunitlindflem1  35069  poimirlem1  35074  poimirlem30  35103  poimirlem32  35105  poimir  35106  ismblfin  35114  volsupnfl  35118  itg2addnclem3  35126  fdc  35199  isfldidl  35522  eldmqsres2  35720  n0elqs  35759  rnxrncnvepres  35824  rnxrnidres  35825  dfcoels  35851  br1cossinres  35863  br1cossinidres  35865  br1cossincnvepres  35866  br1cossxrnidres  35867  br1cossxrncnvepres  35868  br1cossxrncnvssrres  35924  eldmqs1cossres  36069  prtlem10  36177  prter2  36193  islshpat  36329  lshpsmreu  36421  2dim  36782  islpln5  36847  lplnexatN  36875  islvol5  36891  dalem18  36993  dalem20  37005  lhpexle2  37322  lhpexle3  37324  lhpex2leN  37325  4atex2  37389  4atex2-0bOLDN  37391  cdlemftr3  37877  cdlemg17pq  37984  cdlemg19  37996  cdlemg21  37998  cdlemg33d  38021  dva1dim  38297  dih1dimatlem  38641  dihglb2  38654  dvh2dim  38757  mapdrvallem2  38957  mapdpglem3  38987  hdmapglem7a  39239  iunsn  39428  dffltz  39630  elrfirn  39651  isnacs2  39662  isnacs3  39666  sbc2rex  39743  4rexfrabdioph  39754  eldioph4b  39767  fphpd  39772  fiphp3d  39775  rencldnfilem  39776  rmxdioph  39972  expdiophlem1  39977  islnm2  40037  elimaint  40364  cnviun  40366  imaiun1  40367  coiun1  40368  elintima  40369  briunov2  40398  clsk3nimkb  40758  expandrexn  41014  prmunb2  41030  zfregs2VD  41562  evth2f  41659  evthf  41671  ndisj2  41700  fnlimabslt  42336  climbddf  42344  limsupub  42361  limsuppnflem  42367  limsupubuz  42370  limsupre2lem  42381  limsupreuz  42394  limsupvaluz2  42395  cnrefiisplem  42486  cnrefiisp  42487  stoweidlem28  42685  fourierdlem63  42826  fourierdlem65  42828  fourierdlem89  42852  fourierdlem90  42853  fourierdlem91  42854  fourierdlem100  42863  sge0pnfmpt  43099  ovn0  43220  smfaddlem1  43411  smflimlem4  43422  2rexsb  43671  2rexrsb  43672  cbvrex2  43674  2reu8i  43684  copisnmnd  44444  pgrpgt2nabl  44783  islindeps  44876  lindslinindsimp1  44880  lindslinindsimp2  44886  islindeps2  44906  islininds2  44907  isldepslvec2  44908  ldepslinc  44932
 Copyright terms: Public domain W3C validator