Theorem rexbii 3093

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

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rexbiia 3091	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 205   ∈ wcel 2105  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-rex 3071

This theorem is referenced by:  r19.29imd  3117  r19.43  3121  2rexbii  3124  rexnal2  3128  r19.42v  3183  r19.41vv  3211  3reeanv  3214  2ralorOLD  3216  cbvrex2vw  3224  rexcomOLD  3270  rexcom4a  3271  rexcom13  3275  rexrot4  3276  2ex2rexrot  3277  cbvrex2v  3338  rexcom4b  3470  ceqsrex2v  3597  clel5  3606  reu7  3677  2reu5a  3689  0el  4306  n0snor2el  4777  uni0b  4880  iuncom  4945  iuncom4  4946  iuniin  4950  dfiunv2  4979  iunab  4995  iunid  5004  iunsn  5010  iunn0  5011  iunin2  5015  iundif2  5018  iunun  5037  iunxiun  5041  iunpwss  5051  axrep6  5233  inuni  5284  reusv2lem5  5342  iunopab  5497  iunopabOLD  5498  dffr2  5578  dffr2ALT  5579  frc  5580  frminex  5594  dfepfr  5599  epfrc  5600  xpiundi  5682  xpiundir  5683  reliin  5753  iunxpf  5784  cnvuni  5822  dmiun  5849  dmopab2rex  5853  elres  5956  elidinxp  5977  dfima3  5996  dffr3  6031  rniun  6080  xpdifid  6100  dminxp  6112  imaco  6183  coiun  6188  dffr4  6252  frpomin2  6274  tz6.26OLD  6281  sucel  6369  isarep1  6567  isarep1OLD  6568  rexrn  7013  ralrn  7014  elrnrexdmb  7016  fnasrn  7067  rexima  7163  ralima  7164  abrexco  7167  imaiun  7168  fliftcnv  7232  rexrnmpo  7467  iunpw  7675  abrexex2g  7867  el2xptp  7937  soseq  8038  frrlem9  8172  rdglem1  8308  tz7.49  8338  oarec  8456  omeu  8479  qsid  8635  eroveu  8664  ixp0  8782  fimax2g  9146  marypha2lem2  9285  dfsup2  9293  infcllem  9336  dfoi  9360  wemapsolem  9399  zfregcl  9443  zfreg  9444  zfregfr  9454  oemapso  9531  brttrcl2  9563  ttrclresv  9566  zfregs2  9582  infenaleph  9940  isinfcard  9941  kmlem7  10005  kmlem13  10011  fin23lem26  10174  dffin1-5  10237  fin12  10262  numth  10321  ac6n  10334  zorn2lem7  10351  zorng  10353  brdom7disj  10380  brdom6disj  10381  uniwun  10589  axgroth5  10673  axgroth4  10681  grothprim  10683  npomex  10845  genpass  10858  elreal  10980  dfinfre  12049  infrenegsup  12051  uzwo  12744  ublbneg  12766  xrinfmss2  13138  4fvwrd4  13469  fsuppmapnn0fiubex  13805  fsuppmapnn0ub  13808  mptnn0fsuppr  13812  hashge2el2dif  14286  cshwsexa  14627  dfrtrclrec2  14860  rexanuz  15148  rexfiuz  15150  clim0  15306  cbvsum  15498  incexc2  15641  cbvprod  15716  fprodle  15797  iprodmul  15804  divalglem10  16202  divalgb  16204  ncoprmlnprm  16521  pythagtriplem2  16607  pythagtriplem19  16623  pythagtrip  16624  pceu  16636  prmreclem6  16711  4sqlem12  16746  cshwshashlem1  16886  cshwshash  16895  imasaddfnlem  17328  isdrs2  18113  smndex1mgm  18634  smndex1n0mnd  18639  pmtrprfvalrn  19184  pgpfac1lem5  19769  dvdsrval  19974  opprunit  19990  lsmspsn  20444  lsmelval2  20445  islpidl  20615  mat1dimelbas  21718  mat1dimbas  21719  mdetunilem8  21866  pmatcollpw2lem  22024  tgval2  22204  ntreq0  22326  isclo2  22337  neiptopnei  22381  ist0-3  22594  tgcmp  22650  cmpfi  22657  is1stc2  22691  unisngl  22776  xkobval  22835  txtube  22889  txcmplem1  22890  xkococnlem  22908  eltsms  23382  metrest  23778  iscau3  24540  bcth  24591  pmltpc  24712  itg2i1fseq  25018  itg2cn  25026  plyun0  25456  aaliou3lem9  25608  1cubr  26090  dchrvmasumlema  26746  selbergsb  26821  ostth  26885  noseponlem  26910  nosepon  26911  nolt02o  26941  noinfbnd1lem1  26969  noinfbnd1lem4  26972  istrkg2ld  27023  tglowdim1i  27064  legtrid  27154  midex  27300  ishpg  27322  brbtwn2  27475  colinearalg  27480  ax5seg  27508  axpasch  27511  axlowdimlem6  27517  axeuclidlem  27532  axeuclid  27533  elntg2  27555  umgr2edg1  27780  umgr2edgneu  27783  nbgrsym  27932  isuvtx  27964  usgr2pth0  28334  wlkiswwlksupgr2  28443  clwwlknun  28677  4cycl2vnunb  28855  fusgreg2wsp  28901  lpni  29043  nmobndseqi  29342  hhcmpl  29763  shne0i  30011  nmcopexi  30590  nmcfnexi  30614  cdj3lem3b  31003  rexcom4f  31020  reuxfrdf  31040  iunin1f  31097  ofpreima  31202  intimafv  31243  fpwrelmapffslem  31267  tosglblem  31452  xrnarchi  31638  lsmsnorb  31789  lsmsnorb2  31790  ordtconnlem1  32085  lmdvg  32114  esumfsup  32249  reprsuc  32808  reprdifc  32820  bnj168  32922  bnj1185  32985  bnj1542  33049  bnj865  33115  bnj916  33125  bnj983  33143  bnj1176  33197  bnj1189  33201  bnj1296  33213  bnj1398  33226  bnj1450  33242  bnj1463  33247  nummin  33275  loop1cycl  33311  cvmliftlem15  33472  cvmlift2lem12  33488  satfvsuclem2  33534  satfvsucsuc  33539  satfdm  33543  satf0  33546  dmopab3rexdif  33579  imaeqsexv  33896  dffr5  33926  imaindm  33952  dfon2lem9  33966  poxp2  33988  poxp3  33994  elold  34144  made0  34148  lrrecfr  34191  brbigcup  34291  elfuns  34308  brimage  34319  brimg  34330  dfrecs2  34343  imagesset  34346  brub  34347  brsegle  34501  filnetlem4  34661  bj-rexcom4bv  35157  bj-rexcom4b  35158  bj-elsngl  35247  bj-rest10  35357  bj-restreg  35368  bj-mpomptALT  35388  nlpineqsn  35677  fvineqsneq  35681  iundif1  35849  matunitlindflem1  35871  poimirlem1  35876  poimirlem30  35905  poimirlem32  35907  poimir  35908  ismblfin  35916  volsupnfl  35920  itg2addnclem3  35928  fdc  36001  isfldidl  36324  eldmqsres2  36546  n0elqs  36585  rnxrncnvepres  36660  rnxrnidres  36661  dfcoels  36690  br1cossinres  36707  br1cossinidres  36709  br1cossincnvepres  36710  br1cossxrnidres  36711  br1cossxrncnvepres  36712  br1cossxrncnvssrres  36768  eldmqs1cossres  36919  disjdmqscossss  37063  prtlem10  37125  prter2  37141  islshpat  37277  lshpsmreu  37369  2dim  37731  islpln5  37796  lplnexatN  37824  islvol5  37840  dalem18  37942  dalem20  37954  lhpexle2  38271  lhpexle3  38273  lhpex2leN  38274  4atex2  38338  4atex2-0bOLDN  38340  cdlemftr3  38826  cdlemg17pq  38933  cdlemg19  38945  cdlemg21  38947  cdlemg33d  38970  dva1dim  39246  dih1dimatlem  39590  dihglb2  39603  dvh2dim  39706  mapdrvallem2  39906  mapdpglem3  39936  hdmapglem7a  40188  dffltz  40721  elrfirn  40767  isnacs2  40778  isnacs3  40782  sbc2rex  40859  4rexfrabdioph  40870  eldioph4b  40883  fphpd  40888  fiphp3d  40891  rencldnfilem  40892  rmxdioph  41089  expdiophlem1  41094  islnm2  41154  elimaint  41567  cnviun  41568  imaiun1  41569  coiun1  41570  elintima  41571  briunov2  41600  clsk3nimkb  41960  expandrexn  42219  prmunb2  42239  zfregs2VD  42771  evth2f  42868  evthf  42880  ndisj2  42908  fnlimabslt  43545  climbddf  43553  limsupub  43570  limsuppnflem  43576  limsupubuz  43579  limsupre2lem  43590  limsupreuz  43603  limsupvaluz2  43604  cnrefiisplem  43695  cnrefiisp  43696  stoweidlem28  43894  fourierdlem63  44035  fourierdlem65  44037  fourierdlem89  44061  fourierdlem90  44062  fourierdlem91  44063  fourierdlem100  44072  sge0pnfmpt  44309  ovn0  44430  smfaddlem1  44627  smflimlem4  44638  fsetsniunop  44883  2rexsb  44933  2rexrsb  44934  cbvrex2  44936  2reu8i  44945  copisnmnd  45703  pgrpgt2nabl  46042  islindeps  46134  lindslinindsimp1  46138  lindslinindsimp2  46144  islindeps2  46164  islininds2  46165  isldepslvec2  46166  ldepslinc  46190  sepnsepolem1  46555