Theorem rexbii 3095

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 3093	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 205   ∈ wcel 2107  ∃wrex 3071

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-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.29imd  3119  r19.43  3123  2rexbii  3130  rexnal2  3136  r19.42v  3191  r19.41vv  3225  3reeanv  3228  2ralorOLD  3230  cbvrex2vw  3240  rexcomOLD  3289  rexcom4a  3290  rexcom13  3294  rexrot4  3295  2ex2rexrot  3296  cbvrex2v  3366  rexcom4b  3504  ceqsrex2v  3646  clel5  3655  reu7  3728  2reu5a  3740  0el  4360  n0snor2el  4834  uni0b  4937  iuncom  5004  iuncom4  5005  iuniin  5009  dfiunv2  5038  iunab  5054  iunid  5063  iunsn  5069  iunn0  5070  iunin2  5074  iundif2  5077  iunun  5096  iunxiun  5100  iunpwss  5110  axrep6  5292  inuni  5343  reusv2lem5  5400  iunopab  5559  iunopabOLD  5560  dffr2  5640  dffr2ALT  5641  frc  5642  frminex  5656  dfepfr  5661  epfrc  5662  xpiundi  5745  xpiundir  5746  reliin  5816  iunxpf  5847  cnvuni  5885  dmiun  5912  dmopab2rex  5916  elres  6019  elidinxp  6042  dfima3  6061  dffr3  6096  rniun  6145  xpdifid  6165  dminxp  6177  imaco  6248  coiun  6253  imaindm  6296  dffr4  6318  frpomin2  6340  tz6.26OLD  6347  sucel  6436  isarep1  6635  isarep1OLD  6636  rexrn  7086  ralrn  7087  elrnrexdmb  7089  fnasrn  7140  rexima  7236  ralima  7237  abrexco  7240  imaiun  7241  fliftcnv  7305  imaeqsexv  7357  rexrnmpo  7545  imaeqexov  7642  iunpw  7755  abrexex2g  7948  el2xptp  8018  poxp2  8126  poxp3  8133  soseq  8142  frrlem9  8276  rdglem1  8412  tz7.49  8442  oarec  8559  omeu  8582  qsid  8774  eroveu  8803  ixp0  8922  fimax2g  9286  marypha2lem2  9428  dfsup2  9436  infcllem  9479  dfoi  9503  wemapsolem  9542  zfregcl  9586  zfreg  9587  zfregfr  9597  oemapso  9674  brttrcl2  9706  ttrclresv  9709  zfregs2  9725  infenaleph  10083  isinfcard  10084  kmlem7  10148  kmlem13  10154  fin23lem26  10317  dffin1-5  10380  fin12  10405  numth  10464  ac6n  10477  zorn2lem7  10494  zorng  10496  brdom7disj  10523  brdom6disj  10524  uniwun  10732  axgroth5  10816  axgroth4  10824  grothprim  10826  npomex  10988  genpass  11001  elreal  11123  dfinfre  12192  infrenegsup  12194  uzwo  12892  ublbneg  12914  xrinfmss2  13287  4fvwrd4  13618  fsuppmapnn0fiubex  13954  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  hashge2el2dif  14438  cshwsexa  14771  dfrtrclrec2  15002  rexanuz  15289  rexfiuz  15291  clim0  15447  cbvsum  15638  incexc2  15781  cbvprod  15856  fprodle  15937  iprodmul  15944  divalglem10  16342  divalgb  16344  ncoprmlnprm  16661  pythagtriplem2  16747  pythagtriplem19  16763  pythagtrip  16764  pceu  16776  prmreclem6  16851  4sqlem12  16886  cshwshashlem1  17026  cshwshash  17035  imasaddfnlem  17471  isdrs2  18256  smndex1mgm  18785  smndex1n0mnd  18790  pmtrprfvalrn  19351  pgpfac1lem5  19944  dvdsrval  20168  opprunit  20184  lsmspsn  20688  lsmelval2  20689  islpidl  20877  mat1dimelbas  21965  mat1dimbas  21966  mdetunilem8  22113  pmatcollpw2lem  22271  tgval2  22451  ntreq0  22573  isclo2  22584  neiptopnei  22628  ist0-3  22841  tgcmp  22897  cmpfi  22904  is1stc2  22938  unisngl  23023  xkobval  23082  txtube  23136  txcmplem1  23137  xkococnlem  23155  eltsms  23629  metrest  24025  iscau3  24787  bcth  24838  pmltpc  24959  itg2i1fseq  25265  itg2cn  25273  plyun0  25703  aaliou3lem9  25855  1cubr  26337  dchrvmasumlema  26993  selbergsb  27068  ostth  27132  noseponlem  27157  nosepon  27158  nolt02o  27188  noinfbnd1lem1  27216  noinfbnd1lem4  27219  cuteq1  27324  elold  27354  made0  27358  lrrecfr  27417  sleadd1  27462  addsuniflem  27474  addsasslem1  27476  addsasslem2  27477  mulsrid  27559  mulsuniflem  27594  addsdilem1  27596  addsdilem2  27597  mulsasslem1  27608  mulsasslem2  27609  istrkg2ld  27701  tglowdim1i  27742  legtrid  27832  midex  27978  ishpg  28000  brbtwn2  28153  colinearalg  28158  ax5seg  28186  axpasch  28189  axlowdimlem6  28195  axeuclidlem  28210  axeuclid  28211  elntg2  28233  umgr2edg1  28458  umgr2edgneu  28461  nbgrsym  28610  isuvtx  28642  usgr2pth0  29012  wlkiswwlksupgr2  29121  clwwlknun  29355  4cycl2vnunb  29533  fusgreg2wsp  29579  lpni  29721  nmobndseqi  30020  hhcmpl  30441  shne0i  30689  nmcopexi  31268  nmcfnexi  31292  cdj3lem3b  31681  rexcom4f  31698  reuxfrdf  31719  iunin1f  31777  ofpreima  31878  intimafv  31920  fpwrelmapffslem  31945  tosglblem  32132  xrnarchi  32318  isdrng4  32384  dvdsrspss  32480  lsmsnorb  32490  lsmsnorb2  32491  ordtconnlem1  32893  lmdvg  32922  esumfsup  33057  reprsuc  33616  reprdifc  33628  bnj168  33730  bnj1185  33793  bnj1542  33857  bnj865  33923  bnj916  33933  bnj983  33951  bnj1176  34005  bnj1189  34009  bnj1296  34021  bnj1398  34034  bnj1450  34050  bnj1463  34055  nummin  34083  loop1cycl  34117  cvmliftlem15  34278  cvmlift2lem12  34294  satfvsuclem2  34340  satfvsucsuc  34345  satfdm  34349  satf0  34352  dmopab3rexdif  34385  dffr5  34713  dfon2lem9  34752  brbigcup  34859  elfuns  34876  brimage  34887  brimg  34898  dfrecs2  34911  imagesset  34914  brub  34915  brsegle  35069  filnetlem4  35255  bj-rexcom4bv  35751  bj-rexcom4b  35752  bj-elsngl  35838  bj-rest10  35958  bj-restreg  35969  bj-mpomptALT  35989  nlpineqsn  36278  fvineqsneq  36282  iundif1  36451  matunitlindflem1  36473  poimirlem1  36478  poimirlem30  36507  poimirlem32  36509  poimir  36510  ismblfin  36518  volsupnfl  36522  itg2addnclem3  36530  fdc  36602  isfldidl  36925  eldmqsres2  37145  n0elqs  37184  rnxrncnvepres  37259  rnxrnidres  37260  dfcoels  37289  br1cossinres  37306  br1cossinidres  37308  br1cossincnvepres  37309  br1cossxrnidres  37310  br1cossxrncnvepres  37311  br1cossxrncnvssrres  37367  eldmqs1cossres  37518  disjdmqscossss  37662  prtlem10  37724  prter2  37740  islshpat  37876  lshpsmreu  37968  2dim  38330  islpln5  38395  lplnexatN  38423  islvol5  38439  dalem18  38541  dalem20  38553  lhpexle2  38870  lhpexle3  38872  lhpex2leN  38873  4atex2  38937  4atex2-0bOLDN  38939  cdlemftr3  39425  cdlemg17pq  39532  cdlemg19  39544  cdlemg21  39546  cdlemg33d  39569  dva1dim  39845  dih1dimatlem  40189  dihglb2  40202  dvh2dim  40305  mapdrvallem2  40505  mapdpglem3  40535  hdmapglem7a  40787  dffltz  41373  elrfirn  41419  isnacs2  41430  isnacs3  41434  sbc2rex  41511  4rexfrabdioph  41522  eldioph4b  41535  fphpd  41540  fiphp3d  41543  rencldnfilem  41544  rmxdioph  41741  expdiophlem1  41746  islnm2  41806  onmaxnelsup  41958  onsupnmax  41963  onsupuni  41964  onsupmaxb  41974  tfsconcatlem  42072  tfsconcatrn  42078  oadif1lem  42115  oadif1  42116  elimaint  42386  cnviun  42387  imaiun1  42388  coiun1  42389  elintima  42390  briunov2  42419  clsk3nimkb  42777  expandrexn  43036  prmunb2  43056  zfregs2VD  43588  evth2f  43685  evthf  43697  ndisj2  43724  rexanuz2nf  44190  fnlimabslt  44382  climbddf  44390  limsupub  44407  limsuppnflem  44413  limsupubuz  44416  limsupre2lem  44427  limsupreuz  44440  limsupvaluz2  44441  cnrefiisplem  44532  cnrefiisp  44533  stoweidlem28  44731  fourierdlem63  44872  fourierdlem65  44874  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem100  44909  sge0pnfmpt  45148  ovn0  45269  smfaddlem1  45466  smflimlem4  45477  fsetsniunop  45746  2rexsb  45796  2rexrsb  45797  cbvrex2  45799  2reu8i  45808  copisnmnd  46566  pgrpgt2nabl  46996  islindeps  47088  lindslinindsimp1  47092  lindslinindsimp2  47098  islindeps2  47118  islininds2  47119  isldepslvec2  47120  ldepslinc  47144  sepnsepolem1  47508