Theorem rexbii 3087

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  r19.29imd  3105  r19.43  3108  3r19.43  3109  2rexbii  3116  rexnal2  3122  r19.42v  3172  r19.41vv  3210  3reeanv  3213  cbvrex2vw  3223  rexcom4a  3270  rexcom13  3273  rexrot4  3274  2ex2rexrot  3275  cbvrex2v  3334  rexcom4b  3464  ceqsrex2v  3603  clel5  3610  reu7  3680  2reu5a  3692  0el  4298  n0snor2el  4771  uni0b  4871  iuncom  4936  iuncom4  4937  iuniin  4941  dfiunv2  4970  iunab  4988  iunid  4997  iunsn  5002  iunn0  5003  iunin2  5007  iundif2  5010  iunun  5029  iunxiun  5033  iunpwss  5043  axrep6OLD  5216  inuni  5285  reusv2lem5  5338  iunopab  5508  dffr2  5586  dffr2ALT  5587  frc  5588  frminex  5604  dfepfr  5609  epfrc  5610  xpiundi  5696  xpiundir  5697  reliin  5767  iunxpf  5797  cnvuni  5835  dmiun  5862  dmopab2rex  5866  elres  5979  elidinxp  6003  dfima3  6022  dffr3  6058  rniun  6105  xpdifid  6126  dminxp  6138  imaco  6209  coiun  6215  imaindm  6257  dffr4  6278  frpomin2  6299  sucel  6393  isarep1  6581  rexrn  7035  ralrn  7036  elrnrexdmb  7038  fnasrn  7094  ralima  7188  reximaOLD  7190  ralimaOLD  7191  abrexco  7195  imaiun  7196  fliftcnv  7262  imaeqsexvOLD  7314  rexrnmpo  7503  imaeqexov  7601  iunpw  7721  abrexex2g  7913  el2xptp  7984  poxp2  8090  poxp3  8097  soseq  8106  frrlem9  8241  rdglem1  8351  tz7.49  8381  oarec  8494  omeu  8517  qsid  8725  eroveu  8756  ixp0  8876  fimax2g  9193  marypha2lem2  9346  dfsup2  9354  infcllem  9398  dfoi  9423  wemapsolem  9462  zfregcl  9506  zfregclOLD  9507  zfreg  9508  zfregfr  9523  oemapso  9601  brttrcl2  9633  ttrclresv  9636  zfregs2  9652  infenaleph  10011  isinfcard  10012  kmlem7  10077  kmlem13  10083  fin23lem26  10245  dffin1-5  10308  fin12  10333  numth  10392  ac6n  10405  zorn2lem7  10422  zorng  10424  brdom7disj  10451  brdom6disj  10452  uniwun  10661  axgroth5  10745  axgroth4  10753  grothprim  10755  npomex  10917  genpass  10930  elreal  11052  dfinfre  12135  infrenegsup  12137  uzwo  12859  ublbneg  12881  xrinfmss2  13261  4fvwrd4  13600  fsuppmapnn0fiubex  13952  fsuppmapnn0ub  13955  mptnn0fsuppr  13959  hashge2el2dif  14440  cshwsexa  14784  dfrtrclrec2  15018  rexanuz  15306  rexfiuz  15308  clim0  15466  cbvsum  15655  cbvsumv  15656  incexc2  15801  cbvprod  15876  cbvprodv  15877  prodeq1i  15879  fprodle  15959  iprodmul  15966  divalglem10  16369  divalgb  16371  ncoprmlnprm  16696  pythagtriplem2  16786  pythagtriplem19  16802  pythagtrip  16803  pceu  16815  prmreclem6  16890  4sqlem12  16925  cshwshashlem1  17064  cshwshash  17073  imasaddfnlem  17490  isdrs2  18270  chnfi  18598  smndex1mgm  18876  smndex1n0mnd  18881  pmtrprfvalrn  19461  pgpfac1lem5  20054  dvdsrval  20339  opprunit  20355  lsmspsn  21081  lsmelval2  21082  islpidl  21325  pzriprnglem3  21465  pzriprnglem10  21472  mat1dimelbas  22461  mat1dimbas  22462  mdetunilem8  22609  pmatcollpw2lem  22767  tgval2  22946  ntreq0  23067  isclo2  23078  neiptopnei  23122  ist0-3  23335  tgcmp  23391  cmpfi  23398  is1stc2  23432  unisngl  23517  xkobval  23576  txtube  23630  txcmplem1  23631  xkococnlem  23649  eltsms  24123  metrest  24514  iscau3  25270  bcth  25321  pmltpc  25442  itg2i1fseq  25747  itg2cn  25755  plyun0  26187  aaliou3lem9  26341  1cubr  26831  dchrvmasumlema  27488  selbergsb  27563  ostth  27627  noseponlem  27653  nosepon  27654  nolt02o  27684  noinfbnd1lem1  27712  noinfbnd1lem4  27715  cuteq1  27834  elold  27876  made0  27880  lrrecfr  27960  leadds1  28006  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  mulsrid  28130  mulsuniflem  28166  addsdilem1  28168  addsdilem2  28169  mulsasslem1  28180  mulsasslem2  28181  z12sge0  28500  elreno2  28512  renegscl  28515  istrkg2ld  28553  tglowdim1i  28594  legtrid  28684  midex  28830  ishpg  28852  brbtwn2  28999  colinearalg  29004  ax5seg  29032  axpasch  29035  axlowdimlem6  29041  axeuclidlem  29056  axeuclid  29057  elntg2  29079  umgr2edg1  29305  umgr2edgneu  29308  nbgrsym  29457  isuvtx  29489  usgr2pth0  29858  wlkiswwlksupgr2  29970  clwwlknun  30207  4cycl2vnunb  30385  fusgreg2wsp  30431  lpni  30576  nmobndseqi  30875  hhcmpl  31296  shne0i  31544  nmcopexi  32123  nmcfnexi  32147  cdj3lem3b  32536  rexcom4f  32562  reuxfrdf  32585  iunin1f  32653  ofpreima  32764  intimafv  32810  fpwrelmapffslem  32831  tosglblem  33060  xrnarchi  33272  isunit2  33328  isdrng4  33386  dvdsrspss  33477  lsmsnorb  33481  lsmsnorb2  33482  1arithufdlem4  33637  constrconj  33936  ordtconnlem1  34115  lmdvg  34144  esumfsup  34261  reprsuc  34806  reprdifc  34818  bnj168  34920  bnj1185  34982  bnj1542  35046  bnj865  35112  bnj916  35122  bnj983  35140  bnj1176  35194  bnj1189  35198  bnj1296  35210  bnj1398  35223  bnj1450  35239  bnj1463  35244  nummin  35281  fineqvnttrclse  35312  axregszf  35317  onvf1odlem1  35338  loop1cycl  35372  cvmliftlem15  35533  cvmlift2lem12  35549  satfvsuclem2  35595  satfvsucsuc  35600  satfdm  35604  satf0  35607  dmopab3rexdif  35640  rexxfr3dALT  35874  dffr5  35989  dfon2lem9  36024  brbigcup  36131  elfuns  36148  brimage  36159  brimg  36170  dfrecs2  36185  imagesset  36188  brub  36189  brsegle  36343  sumeq2si  36437  prodeq2si  36439  cbvprodvw2  36482  filnetlem4  36616  bj-rexcom4bv  37242  bj-rexcom4b  37243  bj-elsngl  37328  bj-axseprep  37434  bj-rest10  37453  bj-restreg  37464  bj-mpomptALT  37484  nlpineqsn  37777  fvineqsneq  37781  iundif1  37968  matunitlindflem1  37990  poimirlem1  37995  poimirlem30  38024  poimirlem32  38026  poimir  38027  ismblfin  38035  volsupnfl  38039  itg2addnclem3  38047  fdc  38119  isfldidl  38442  eldmqsres2  38668  n0elqs  38706  rnxrncnvepres  38797  rnxrnidres  38798  dfcoels  38894  br1cossinres  38911  br1cossinidres  38913  br1cossincnvepres  38914  br1cossxrnidres  38915  br1cossxrncnvepres  38916  br1cossxrncnvssrres  38962  eldmqs1cossres  39118  disjdmqscossss  39280  prtlem10  39364  prter2  39380  islshpat  39516  lshpsmreu  39608  2dim  39969  islpln5  40034  lplnexatN  40062  islvol5  40078  dalem18  40180  dalem20  40192  lhpexle2  40509  lhpexle3  40511  lhpex2leN  40512  4atex2  40576  4atex2-0bOLDN  40578  cdlemftr3  41064  cdlemg17pq  41171  cdlemg19  41183  cdlemg21  41185  cdlemg33d  41208  dva1dim  41484  dih1dimatlem  41828  dihglb2  41841  dvh2dim  41944  mapdrvallem2  42144  mapdpglem3  42174  hdmapglem7a  42426  hashnexinjle  42621  aks6d1c5  42631  supinf  42733  fimgmcyclem  43026  dffltz  43091  elrfirn  43151  isnacs2  43162  isnacs3  43166  sbc2rex  43241  4rexfrabdioph  43250  eldioph4b  43263  fphpd  43268  fiphp3d  43271  rencldnfilem  43272  rmxdioph  43468  expdiophlem1  43473  islnm2  43530  onmaxnelsup  43675  onsupnmax  43680  onsupuni  43681  onsupmaxb  43691  tfsconcatlem  43788  tfsconcatrn  43794  oadif1lem  43831  oadif1  43832  elimaint  44100  cnviun  44101  imaiun1  44102  coiun1  44103  elintima  44104  briunov2  44133  clsk3nimkb  44491  expandrexn  44742  prmunb2  44762  zfregs2VD  45291  n0abso  45427  sswfaxreg  45438  evth2f  45470  evthf  45482  ndisj2  45506  rexanuz2nf  45942  fnlimabslt  46129  climbddf  46137  limsupub  46154  limsuppnflem  46160  limsupubuz  46163  limsupre2lem  46174  limsupreuz  46187  limsupvaluz2  46188  cnrefiisplem  46279  cnrefiisp  46280  stoweidlem28  46478  fourierdlem63  46619  fourierdlem65  46621  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem100  46656  sge0pnfmpt  46895  ovn0  47016  smfaddlem1  47213  smflimlem4  47224  fsetsniunop  47519  2rexsb  47571  2rexrsb  47572  cbvrex2  47574  2reu8i  47583  clnbgrsym  48336  isubgr3stgrlem6  48469  copisnmnd  48667  pgrpgt2nabl  48864  islindeps  48951  lindslinindsimp1  48955  lindslinindsimp2  48961  islindeps2  48981  islininds2  48982  isldepslvec2  48983  ldepslinc  49007  sepnsepolem1  49419