Theorem rexbii 3092

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

Syntax hints:   ↔ wb 206   ∈ wcel 2106  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  r19.29imd  3116  r19.43  3120  2rexbii  3127  rexnal2  3133  r19.42v  3189  r19.41vv  3225  3reeanv  3228  2ralorOLD  3230  cbvrex2vw  3240  rexcomOLD  3289  rexcom4a  3290  rexcom13  3294  rexrot4  3295  2ex2rexrot  3296  cbvrex2v  3367  rexcom4b  3511  ceqsrex2v  3658  clel5  3665  reu7  3741  2reu5a  3753  0el  4369  n0snor2el  4838  uni0b  4938  iuncom  5004  iuncom4  5005  iuniin  5009  dfiunv2  5040  iunab  5056  iunid  5065  iunsn  5071  iunn0  5072  iunin2  5076  iundif2  5079  iunun  5098  iunxiun  5102  iunpwss  5112  axrep6OLD  5295  inuni  5356  reusv2lem5  5408  iunopab  5569  iunopabOLD  5570  dffr2  5650  dffr2ALT  5651  frc  5652  frminex  5668  dfepfr  5673  epfrc  5674  xpiundi  5759  xpiundir  5760  reliin  5830  iunxpf  5862  cnvuni  5900  dmiun  5927  dmopab2rex  5931  elres  6040  elidinxp  6064  dfima3  6083  dffr3  6120  rniun  6170  xpdifid  6190  dminxp  6202  imaco  6273  coiun  6278  imaindm  6321  dffr4  6343  frpomin2  6364  tz6.26OLD  6371  sucel  6460  isarep1  6657  isarep1OLD  6658  rexrn  7107  ralrn  7108  elrnrexdmb  7110  fnasrn  7165  ralima  7257  reximaOLD  7259  ralimaOLD  7260  abrexco  7264  imaiun  7265  fliftcnv  7331  imaeqsexvOLD  7383  rexrnmpo  7573  imaeqexov  7671  iunpw  7790  abrexex2g  7988  el2xptp  8059  poxp2  8167  poxp3  8174  soseq  8183  frrlem9  8318  rdglem1  8454  tz7.49  8484  oarec  8599  omeu  8622  qsid  8822  eroveu  8851  ixp0  8970  fimax2g  9320  marypha2lem2  9474  dfsup2  9482  infcllem  9525  dfoi  9549  wemapsolem  9588  zfregcl  9632  zfreg  9633  zfregfr  9643  oemapso  9720  brttrcl2  9752  ttrclresv  9755  zfregs2  9771  infenaleph  10129  isinfcard  10130  kmlem7  10195  kmlem13  10201  fin23lem26  10363  dffin1-5  10426  fin12  10451  numth  10510  ac6n  10523  zorn2lem7  10540  zorng  10542  brdom7disj  10569  brdom6disj  10570  uniwun  10778  axgroth5  10862  axgroth4  10870  grothprim  10872  npomex  11034  genpass  11047  elreal  11169  dfinfre  12247  infrenegsup  12249  uzwo  12951  ublbneg  12973  xrinfmss2  13350  4fvwrd4  13685  fsuppmapnn0fiubex  14030  fsuppmapnn0ub  14033  mptnn0fsuppr  14037  hashge2el2dif  14516  cshwsexa  14859  dfrtrclrec2  15094  rexanuz  15381  rexfiuz  15383  clim0  15539  cbvsum  15728  cbvsumv  15729  incexc2  15871  cbvprod  15946  cbvprodv  15947  prodeq1i  15949  fprodle  16029  iprodmul  16036  divalglem10  16436  divalgb  16438  ncoprmlnprm  16762  pythagtriplem2  16851  pythagtriplem19  16867  pythagtrip  16868  pceu  16880  prmreclem6  16955  4sqlem12  16990  cshwshashlem1  17130  cshwshash  17139  imasaddfnlem  17575  isdrs2  18364  smndex1mgm  18933  smndex1n0mnd  18938  pmtrprfvalrn  19521  pgpfac1lem5  20114  dvdsrval  20378  opprunit  20394  lsmspsn  21101  lsmelval2  21102  islpidl  21353  pzriprnglem3  21512  pzriprnglem10  21519  mat1dimelbas  22493  mat1dimbas  22494  mdetunilem8  22641  pmatcollpw2lem  22799  tgval2  22979  ntreq0  23101  isclo2  23112  neiptopnei  23156  ist0-3  23369  tgcmp  23425  cmpfi  23432  is1stc2  23466  unisngl  23551  xkobval  23610  txtube  23664  txcmplem1  23665  xkococnlem  23683  eltsms  24157  metrest  24553  iscau3  25326  bcth  25377  pmltpc  25499  itg2i1fseq  25805  itg2cn  25813  plyun0  26251  aaliou3lem9  26407  1cubr  26900  dchrvmasumlema  27559  selbergsb  27634  ostth  27698  noseponlem  27724  nosepon  27725  nolt02o  27755  noinfbnd1lem1  27783  noinfbnd1lem4  27786  cuteq1  27893  elold  27923  made0  27927  lrrecfr  27991  sleadd1  28037  addsuniflem  28049  addsasslem1  28051  addsasslem2  28052  mulsrid  28154  mulsuniflem  28190  addsdilem1  28192  addsdilem2  28193  mulsasslem1  28204  mulsasslem2  28205  renegscl  28445  istrkg2ld  28483  tglowdim1i  28524  legtrid  28614  midex  28760  ishpg  28782  brbtwn2  28935  colinearalg  28940  ax5seg  28968  axpasch  28971  axlowdimlem6  28977  axeuclidlem  28992  axeuclid  28993  elntg2  29015  umgr2edg1  29243  umgr2edgneu  29246  nbgrsym  29395  isuvtx  29427  usgr2pth0  29798  wlkiswwlksupgr2  29907  clwwlknun  30141  4cycl2vnunb  30319  fusgreg2wsp  30365  lpni  30509  nmobndseqi  30808  hhcmpl  31229  shne0i  31477  nmcopexi  32056  nmcfnexi  32080  cdj3lem3b  32469  rexcom4f  32497  reuxfrdf  32519  iunin1f  32578  ofpreima  32682  intimafv  32726  fpwrelmapffslem  32750  tosglblem  32949  xrnarchi  33174  isunit2  33230  isdrng4  33279  dvdsrspss  33395  lsmsnorb  33399  lsmsnorb2  33400  1arithufdlem4  33555  constrconj  33750  ordtconnlem1  33885  lmdvg  33914  esumfsup  34051  reprsuc  34609  reprdifc  34621  bnj168  34723  bnj1185  34786  bnj1542  34850  bnj865  34916  bnj916  34926  bnj983  34944  bnj1176  34998  bnj1189  35002  bnj1296  35014  bnj1398  35027  bnj1450  35043  bnj1463  35048  nummin  35084  loop1cycl  35122  cvmliftlem15  35283  cvmlift2lem12  35299  satfvsuclem2  35345  satfvsucsuc  35350  satfdm  35354  satf0  35357  dmopab3rexdif  35390  rexxfr3dALT  35624  dffr5  35734  dfon2lem9  35773  brbigcup  35880  elfuns  35897  brimage  35908  brimg  35919  dfrecs2  35932  imagesset  35935  brub  35936  brsegle  36090  sumeq2si  36184  prodeq2si  36186  cbvprodvw2  36230  filnetlem4  36364  bj-rexcom4bv  36865  bj-rexcom4b  36866  bj-elsngl  36951  bj-rest10  37071  bj-restreg  37082  bj-mpomptALT  37102  nlpineqsn  37391  fvineqsneq  37395  iundif1  37581  matunitlindflem1  37603  poimirlem1  37608  poimirlem30  37637  poimirlem32  37639  poimir  37640  ismblfin  37648  volsupnfl  37652  itg2addnclem3  37660  fdc  37732  isfldidl  38055  eldmqsres2  38270  n0elqs  38308  rnxrncnvepres  38382  rnxrnidres  38383  dfcoels  38412  br1cossinres  38429  br1cossinidres  38431  br1cossincnvepres  38432  br1cossxrnidres  38433  br1cossxrncnvepres  38434  br1cossxrncnvssrres  38490  eldmqs1cossres  38641  disjdmqscossss  38785  prtlem10  38847  prter2  38863  islshpat  38999  lshpsmreu  39091  2dim  39453  islpln5  39518  lplnexatN  39546  islvol5  39562  dalem18  39664  dalem20  39676  lhpexle2  39993  lhpexle3  39995  lhpex2leN  39996  4atex2  40060  4atex2-0bOLDN  40062  cdlemftr3  40548  cdlemg17pq  40655  cdlemg19  40667  cdlemg21  40669  cdlemg33d  40692  dva1dim  40968  dih1dimatlem  41312  dihglb2  41325  dvh2dim  41428  mapdrvallem2  41628  mapdpglem3  41658  hdmapglem7a  41910  hashnexinjle  42111  aks6d1c5  42121  supinf  42262  fimgmcyclem  42520  dffltz  42621  elrfirn  42683  isnacs2  42694  isnacs3  42698  sbc2rex  42775  4rexfrabdioph  42786  eldioph4b  42799  fphpd  42804  fiphp3d  42807  rencldnfilem  42808  rmxdioph  43005  expdiophlem1  43010  islnm2  43067  onmaxnelsup  43212  onsupnmax  43217  onsupuni  43218  onsupmaxb  43228  tfsconcatlem  43326  tfsconcatrn  43332  oadif1lem  43369  oadif1  43370  elimaint  43639  cnviun  43640  imaiun1  43641  coiun1  43642  elintima  43643  briunov2  43672  clsk3nimkb  44030  expandrexn  44287  prmunb2  44307  zfregs2VD  44839  evth2f  44953  evthf  44965  ndisj2  44991  rexanuz2nf  45443  fnlimabslt  45635  climbddf  45643  limsupub  45660  limsuppnflem  45666  limsupubuz  45669  limsupre2lem  45680  limsupreuz  45693  limsupvaluz2  45694  cnrefiisplem  45785  cnrefiisp  45786  stoweidlem28  45984  fourierdlem63  46125  fourierdlem65  46127  fourierdlem89  46151  fourierdlem90  46152  fourierdlem91  46153  fourierdlem100  46162  sge0pnfmpt  46401  ovn0  46522  smfaddlem1  46719  smflimlem4  46730  fsetsniunop  46999  2rexsb  47051  2rexrsb  47052  cbvrex2  47054  2reu8i  47063  clnbgrsym  47762  isubgr3stgrlem6  47874  copisnmnd  48013  pgrpgt2nabl  48211  islindeps  48299  lindslinindsimp1  48303  lindslinindsimp2  48309  islindeps2  48329  islininds2  48330  isldepslvec2  48331  ldepslinc  48355  sepnsepolem1  48718