Theorem rexbii 3085

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∃wrex 3062

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 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.29imd  3103  r19.43  3106  3r19.43  3107  2rexbii  3114  rexnal2  3120  r19.42v  3170  r19.41vv  3208  3reeanv  3211  cbvrex2vw  3221  rexcom4a  3268  rexcom13  3271  rexrot4  3272  2ex2rexrot  3273  cbvrex2v  3341  rexcom4b  3474  ceqsrex2v  3614  clel5  3621  reu7  3692  2reu5a  3704  0el  4317  n0snor2el  4791  uni0b  4891  iuncom  4956  iuncom4  4957  iuniin  4961  dfiunv2  4991  iunab  5009  iunid  5018  iunsn  5023  iunn0  5024  iunin2  5028  iundif2  5031  iunun  5050  iunxiun  5054  iunpwss  5064  axrep6OLD  5236  inuni  5297  reusv2lem5  5349  iunopab  5515  dffr2  5593  dffr2ALT  5594  frc  5595  frminex  5611  dfepfr  5616  epfrc  5617  xpiundi  5703  xpiundir  5704  reliin  5774  iunxpf  5805  cnvuni  5843  dmiun  5870  dmopab2rex  5874  elres  5987  elidinxp  6011  dfima3  6030  dffr3  6066  rniun  6113  xpdifid  6134  dminxp  6146  imaco  6217  coiun  6223  imaindm  6265  dffr4  6286  frpomin2  6307  sucel  6401  isarep1  6589  rexrn  7041  ralrn  7042  elrnrexdmb  7044  fnasrn  7100  ralima  7193  reximaOLD  7195  ralimaOLD  7196  abrexco  7200  imaiun  7201  fliftcnv  7267  imaeqsexvOLD  7319  rexrnmpo  7508  imaeqexov  7606  iunpw  7726  abrexex2g  7918  el2xptp  7989  poxp2  8095  poxp3  8102  soseq  8111  frrlem9  8246  rdglem1  8356  tz7.49  8386  oarec  8499  omeu  8522  qsid  8730  eroveu  8761  ixp0  8881  fimax2g  9198  marypha2lem2  9351  dfsup2  9359  infcllem  9403  dfoi  9428  wemapsolem  9467  zfregcl  9511  zfregclOLD  9512  zfreg  9513  zfregfr  9525  oemapso  9603  brttrcl2  9635  ttrclresv  9638  zfregs2  9654  infenaleph  10013  isinfcard  10014  kmlem7  10079  kmlem13  10085  fin23lem26  10247  dffin1-5  10310  fin12  10335  numth  10394  ac6n  10407  zorn2lem7  10424  zorng  10426  brdom7disj  10453  brdom6disj  10454  uniwun  10663  axgroth5  10747  axgroth4  10755  grothprim  10757  npomex  10919  genpass  10932  elreal  11054  dfinfre  12135  infrenegsup  12137  uzwo  12836  ublbneg  12858  xrinfmss2  13238  4fvwrd4  13576  fsuppmapnn0fiubex  13927  fsuppmapnn0ub  13930  mptnn0fsuppr  13934  hashge2el2dif  14415  cshwsexa  14759  dfrtrclrec2  14993  rexanuz  15281  rexfiuz  15283  clim0  15441  cbvsum  15630  cbvsumv  15631  incexc2  15773  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  fprodle  15931  iprodmul  15938  divalglem10  16341  divalgb  16343  ncoprmlnprm  16667  pythagtriplem2  16757  pythagtriplem19  16773  pythagtrip  16774  pceu  16786  prmreclem6  16861  4sqlem12  16896  cshwshashlem1  17035  cshwshash  17044  imasaddfnlem  17461  isdrs2  18241  chnfi  18569  smndex1mgm  18844  smndex1n0mnd  18849  pmtrprfvalrn  19429  pgpfac1lem5  20022  dvdsrval  20309  opprunit  20325  lsmspsn  21048  lsmelval2  21049  islpidl  21292  pzriprnglem3  21450  pzriprnglem10  21457  mat1dimelbas  22427  mat1dimbas  22428  mdetunilem8  22575  pmatcollpw2lem  22733  tgval2  22912  ntreq0  23033  isclo2  23044  neiptopnei  23088  ist0-3  23301  tgcmp  23357  cmpfi  23364  is1stc2  23398  unisngl  23483  xkobval  23542  txtube  23596  txcmplem1  23597  xkococnlem  23615  eltsms  24089  metrest  24480  iscau3  25246  bcth  25297  pmltpc  25419  itg2i1fseq  25724  itg2cn  25732  plyun0  26170  aaliou3lem9  26326  1cubr  26820  dchrvmasumlema  27479  selbergsb  27554  ostth  27618  noseponlem  27644  nosepon  27645  nolt02o  27675  noinfbnd1lem1  27703  noinfbnd1lem4  27706  cuteq1  27825  elold  27867  made0  27871  lrrecfr  27951  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  mulsrid  28121  mulsuniflem  28157  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  z12sge0  28491  elreno2  28503  renegscl  28506  istrkg2ld  28544  tglowdim1i  28585  legtrid  28675  midex  28821  ishpg  28843  brbtwn2  28990  colinearalg  28995  ax5seg  29023  axpasch  29026  axlowdimlem6  29032  axeuclidlem  29047  axeuclid  29048  elntg2  29070  umgr2edg1  29296  umgr2edgneu  29299  nbgrsym  29448  isuvtx  29480  usgr2pth0  29850  wlkiswwlksupgr2  29962  clwwlknun  30199  4cycl2vnunb  30377  fusgreg2wsp  30423  lpni  30567  nmobndseqi  30866  hhcmpl  31287  shne0i  31535  nmcopexi  32114  nmcfnexi  32138  cdj3lem3b  32527  rexcom4f  32553  reuxfrdf  32576  iunin1f  32643  ofpreima  32754  intimafv  32800  fpwrelmapffslem  32821  tosglblem  33066  xrnarchi  33277  isunit2  33333  isdrng4  33388  dvdsrspss  33479  lsmsnorb  33483  lsmsnorb2  33484  1arithufdlem4  33639  constrconj  33922  ordtconnlem1  34101  lmdvg  34130  esumfsup  34247  reprsuc  34792  reprdifc  34804  bnj168  34906  bnj1185  34968  bnj1542  35032  bnj865  35098  bnj916  35108  bnj983  35126  bnj1176  35180  bnj1189  35184  bnj1296  35196  bnj1398  35209  bnj1450  35225  bnj1463  35230  nummin  35268  fineqvnttrclse  35299  axregszf  35304  onvf1odlem1  35316  loop1cycl  35350  cvmliftlem15  35511  cvmlift2lem12  35527  satfvsuclem2  35573  satfvsucsuc  35578  satfdm  35582  satf0  35585  dmopab3rexdif  35618  rexxfr3dALT  35852  dffr5  35967  dfon2lem9  36002  brbigcup  36109  elfuns  36126  brimage  36137  brimg  36148  dfrecs2  36163  imagesset  36166  brub  36167  brsegle  36321  sumeq2si  36415  prodeq2si  36417  cbvprodvw2  36460  filnetlem4  36594  bj-rexcom4bv  37124  bj-rexcom4b  37125  bj-elsngl  37210  bj-axseprep  37316  bj-rest10  37335  bj-restreg  37346  bj-mpomptALT  37366  nlpineqsn  37657  fvineqsneq  37661  iundif1  37839  matunitlindflem1  37861  poimirlem1  37866  poimirlem30  37895  poimirlem32  37897  poimir  37898  ismblfin  37906  volsupnfl  37910  itg2addnclem3  37918  fdc  37990  isfldidl  38313  eldmqsres2  38539  n0elqs  38577  rnxrncnvepres  38668  rnxrnidres  38669  dfcoels  38765  br1cossinres  38782  br1cossinidres  38784  br1cossincnvepres  38785  br1cossxrnidres  38786  br1cossxrncnvepres  38787  br1cossxrncnvssrres  38833  eldmqs1cossres  38989  disjdmqscossss  39151  prtlem10  39235  prter2  39251  islshpat  39387  lshpsmreu  39479  2dim  39840  islpln5  39905  lplnexatN  39933  islvol5  39949  dalem18  40051  dalem20  40063  lhpexle2  40380  lhpexle3  40382  lhpex2leN  40383  4atex2  40447  4atex2-0bOLDN  40449  cdlemftr3  40935  cdlemg17pq  41042  cdlemg19  41054  cdlemg21  41056  cdlemg33d  41079  dva1dim  41355  dih1dimatlem  41699  dihglb2  41712  dvh2dim  41815  mapdrvallem2  42015  mapdpglem3  42045  hdmapglem7a  42297  hashnexinjle  42493  aks6d1c5  42503  supinf  42606  fimgmcyclem  42897  dffltz  42986  elrfirn  43046  isnacs2  43057  isnacs3  43061  sbc2rex  43138  4rexfrabdioph  43149  eldioph4b  43162  fphpd  43167  fiphp3d  43170  rencldnfilem  43171  rmxdioph  43367  expdiophlem1  43372  islnm2  43429  onmaxnelsup  43574  onsupnmax  43579  onsupuni  43580  onsupmaxb  43590  tfsconcatlem  43687  tfsconcatrn  43693  oadif1lem  43730  oadif1  43731  elimaint  43999  cnviun  44000  imaiun1  44001  coiun1  44002  elintima  44003  briunov2  44032  clsk3nimkb  44390  expandrexn  44641  prmunb2  44661  zfregs2VD  45190  n0abso  45326  sswfaxreg  45337  evth2f  45369  evthf  45381  ndisj2  45405  rexanuz2nf  45844  fnlimabslt  46031  climbddf  46039  limsupub  46056  limsuppnflem  46062  limsupubuz  46065  limsupre2lem  46076  limsupreuz  46089  limsupvaluz2  46090  cnrefiisplem  46181  cnrefiisp  46182  stoweidlem28  46380  fourierdlem63  46521  fourierdlem65  46523  fourierdlem89  46547  fourierdlem90  46548  fourierdlem91  46549  fourierdlem100  46558  sge0pnfmpt  46797  ovn0  46918  smfaddlem1  47115  smflimlem4  47126  fsetsniunop  47403  2rexsb  47455  2rexrsb  47456  cbvrex2  47458  2reu8i  47467  clnbgrsym  48192  isubgr3stgrlem6  48325  copisnmnd  48523  pgrpgt2nabl  48720  islindeps  48807  lindslinindsimp1  48811  lindslinindsimp2  48817  islindeps2  48837  islininds2  48838  isldepslvec2  48839  ldepslinc  48863  sepnsepolem1  49275