Theorem rexbii 3112

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  r19.29imd  3130  r19.43  3133  3r19.43  3134  2rexbii  3141  rexnal2  3147  r19.42v  3197  r19.41vv  3235  3reeanv  3238  cbvrex2vw  3248  rexcom4a  3295  rexcom13  3298  rexrot4  3299  2ex2rexrot  3300  cbvrex2v  3358  rexcom4b  3486  ceqsrex2v  3618  clel5  3625  reu7  3696  2reu5a  3708  0el  4319  n0snor2el  4799  uni0b  4900  iuncom  4965  iuncom4  4966  iuniin  4970  dfiunv2  4999  iunab  5017  iunid  5026  iunsn  5031  iunn0  5032  iunin2  5036  iundif2  5039  iunun  5060  iunxiun  5064  iunpwss  5074  axrep6OLD  5249  inuni  5322  reusv2lem5  5375  iunopab  5546  dffr2  5624  dffr2ALT  5625  frc  5626  frminex  5642  dfepfr  5647  epfrc  5648  xpiundi  5734  xpiundir  5735  reliin  5806  iunxpf  5836  cnvuni  5878  dmiun  5905  dmopab2rex  5909  elres  6021  elidinxp  6048  dfima3  6067  dffr3  6103  rniun  6147  xpdifid  6167  xpdifcnvepel  6168  dminxp  6180  imaco  6254  coiun  6260  imaindm  6302  dffr4  6323  frpomin2  6344  sucel  6439  isarep1  6626  rexrn  7084  ralrn  7085  elrnrexdmb  7087  fnasrn  7143  ralima  7237  reximaOLD  7239  ralimaOLD  7240  abrexco  7244  imaiun  7245  fliftcnv  7311  imaeqsexvOLD  7363  rexrnmpo  7552  imaeqexov  7650  iunpw  7771  abrexex2g  7962  el2xptp  8033  poxp2  8140  poxp3  8147  soseq  8156  frrlem9  8292  rdglem1  8403  tz7.49  8433  oarec  8548  omeu  8571  qsid  8780  eroveu  8811  ixp0  8930  fimax2g  9247  marypha2lem2  9397  dfsup2  9405  infcllem  9449  dfoi  9474  wemapsolem  9513  zfregcl  9557  zfregclOLD  9558  zfreg  9559  zfregfr  9574  oemapso  9652  brttrcl2  9684  ttrclresv  9687  zfregs2  9703  infenaleph  10076  isinfcard  10077  kmlem7  10141  kmlem13  10147  fin23lem26  10310  dffin1-5  10373  fin12  10398  numth  10457  ac6n  10470  zorn2lem7  10487  zorng  10489  brdom7disj  10516  brdom6disj  10517  uniwun  10726  axgroth5  10810  axgroth4  10818  grothprim  10820  npomex  10982  genpass  10995  elreal  11117  dfinfre  12197  infrenegsup  12199  uzwo  12936  ublbneg  12958  xrinfmss2  13338  4fvwrd4  13678  fsuppmapnn0fiubex  14030  fsuppmapnn0ub  14033  mptnn0fsuppr  14037  hashge2el2dif  14519  cshwsexa  14863  dfrtrclrec2  15097  rexanuz  15399  rexfiuz  15401  clim0  15559  cbvsum  15748  cbvsumv  15749  incexc2  15894  cbvprod  15969  cbvprodv  15970  prodeq1i  15972  fprodle  16052  iprodmul  16059  divalglem10  16461  divalgb  16463  ncoprmlnprm  16788  pythagtriplem2  16878  pythagtriplem19  16894  pythagtrip  16895  pceu  16907  prmreclem6  16982  4sqlem12  17017  cshwshashlem1  17156  cshwshash  17165  imasaddfnlem  17583  isdrs2  18363  chnfi  18691  smndex1mgm  18970  smndex1n0mnd  18975  pmtrprfvalrn  19559  pgpfac1lem5  20152  dvdsrval  20444  opprunit  20460  isdrng4  20826  lsmspsn  21186  lsmelval2  21187  islpidl  21474  pzriprnglem3  21614  pzriprnglem10  21621  mat1dimelbas  22609  mat1dimbas  22610  mdetunilem8  22757  pmatcollpw2lem  22915  tgval2  23094  ntreq0  23215  isclo2  23226  neiptopnei  23270  ist0-3  23483  tgcmp  23539  cmpfi  23546  is1stc2  23580  unisngl  23665  xkobval  23724  txtube  23778  txcmplem1  23779  xkococnlem  23797  eltsms  24271  metrest  24662  iscau3  25418  bcth  25469  pmltpc  25590  itg2i1fseq  25895  itg2cn  25903  plyun0  26335  aaliou3lem9  26494  1cubr  26988  dchrvmasumlema  27645  selbergsb  27720  ostth  27784  noseponlem  27809  nosepon  27810  nolt02o  27840  noinfbnd1lem1  27868  noinfbnd1lem4  27871  cuteq1  27991  elold  28033  made0  28037  lrrecfr  28117  leadds1  28163  addsuniflem  28175  addsasslem1  28177  addsasslem2  28178  mulsrid  28287  mulsuniflem  28323  addsdilem1  28325  addsdilem2  28326  mulsasslem1  28337  mulsasslem2  28338  z12sge0  28657  elreno2  28669  renegscl  28672  istrkg2ld  28710  tglowdim1i  28751  legtrid  28841  midex  28999  ishpg  29022  brbtwn2  29236  colinearalg  29241  ax5seg  29269  axpasch  29272  axlowdimlem6  29278  axeuclidlem  29293  axeuclid  29294  elntg2  29316  umgr2edg1  29542  umgr2edgneu  29545  nbgrsym  29694  isuvtx  29726  usgr2pth0  30095  wlkiswwlksupgr2  30207  clwwlknun  30444  4cycl2vnunb  30622  fusgreg2wsp  30668  lpni  30813  nmobndseqi  31112  hhcmpl  31533  shne0i  31781  nmcopexi  32360  nmcfnexi  32384  cdj3lem3b  32773  rexcom4f  32796  reuxfrdf  32818  iunin1f  32883  ofpreima  32991  intimafv  33037  fpwrelmapffslem  33058  tosglblem  33275  xrnarchi  33485  isunit2  33540  dvdsrspss  33681  lsmsnorb  33685  lsmsnorb2  33686  1arithufdlem4  33818  constrconj  34116  ordtconnlem1  34295  lmdvg  34324  esumfsup  34441  reprsuc  34983  reprdifc  34995  bnj168  35100  bnj1185  35162  bnj1542  35226  bnj865  35292  bnj916  35302  bnj983  35320  bnj1176  35374  bnj1189  35378  bnj1296  35390  bnj1398  35403  bnj1450  35419  bnj1463  35424  nummin  35465  fineqvnttrclse  35518  axregszf  35523  onvf1odlem1  35568  loop1cycl  35610  cvmliftlem15  35771  cvmlift2lem12  35787  satfvsuclem2  35833  satfvsucsuc  35838  satfdm  35842  satf0  35845  dmopab3rexdif  35878  rexxfr3dALT  36112  dffr5  36227  dfon2lem9  36262  brbigcup  36369  elfuns  36386  brimage  36397  brimg  36408  dfrecs2  36423  imagesset  36426  brub  36427  brsegle  36581  sumeq2si  36695  prodeq2si  36697  cbvprodvw2  36740  filnetlem4  36873  bj-rexcom4bv  37498  bj-rexcom4b  37499  bj-elsngl  37585  bj-axseprep  37692  bj-rest10  37711  bj-restreg  37722  bj-mpomptALT  37742  nlpineqsn  38035  fvineqsneq  38039  iundif1  38226  matunitlindflem1  38248  poimirlem1  38253  poimirlem30  38282  poimirlem32  38284  poimir  38285  ismblfin  38293  volsupnfl  38297  itg2addnclem3  38305  fdc  38377  isfldidl  38700  eldmqsres2  38924  n0elqs  38962  rnxrncnvepres  39053  rnxrnidres  39054  dfcoels  39150  br1cossinres  39167  br1cossinidres  39169  br1cossincnvepres  39170  br1cossxrnidres  39171  br1cossxrncnvepres  39172  br1cossxrncnvssrres  39218  eldmqs1cossres  39374  disjdmqscossss  39536  prtlem10  39620  prter2  39636  islshpat  39772  lshpsmreu  39864  2dim  40225  islpln5  40290  lplnexatN  40318  islvol5  40334  dalem18  40436  dalem20  40448  lhpexle2  40765  lhpexle3  40767  lhpex2leN  40768  4atex2  40832  4atex2-0bOLDN  40834  cdlemftr3  41320  cdlemg17pq  41427  cdlemg19  41439  cdlemg21  41441  cdlemg33d  41464  dva1dim  41740  dih1dimatlem  42084  dihglb2  42097  dvh2dim  42200  mapdrvallem2  42400  mapdpglem3  42430  hdmapglem7a  42682  hashnexinjle  42877  aks6d1c5  42887  supinf  42991  fimgmcyclem  43284  dffltz  43349  elrfirn  43409  isnacs2  43420  isnacs3  43424  sbc2rex  43499  4rexfrabdioph  43508  eldioph4b  43521  fphpd  43526  fiphp3d  43529  rencldnfilem  43530  rmxdioph  43726  expdiophlem1  43731  islnm2  43788  onmaxnelsup  43933  onsupnmax  43938  onsupuni  43939  onsupmaxb  43949  tfsconcatlem  44046  tfsconcatrn  44052  oadif1lem  44089  oadif1  44090  elimaint  44358  cnviun  44359  imaiun1  44360  coiun1  44361  elintima  44362  briunov2  44391  clsk3nimkb  44749  expandrexn  44984  prmunb2  45004  zfregs2VD  45532  n0abso  45668  sswfaxreg  45679  evth2f  45718  evthf  45730  ndisj2  45754  rexanuz2nf  46189  fnlimabslt  46376  climbddf  46384  limsupub  46401  limsuppnflem  46407  limsupubuz  46410  limsupre2lem  46421  limsupreuz  46434  limsupvaluz2  46435  cnrefiisplem  46526  cnrefiisp  46527  stoweidlem28  46725  fourierdlem63  46866  fourierdlem65  46868  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem100  46903  sge0pnfmpt  47142  ovn0  47263  smfaddlem1  47460  smflimlem4  47471  fsetsniunop  47769  2rexsb  47821  2rexrsb  47822  cbvrex2  47824  2reu8i  47833  clnbgrsym  48586  isubgr3stgrlem6  48719  copisnmnd  48917  pgrpgt2nabl  49129  islindeps  49216  lindslinindsimp1  49220  lindslinindsimp2  49226  islindeps2  49246  islininds2  49247  isldepslvec2  49248  ldepslinc  49272  sepnsepolem1  49683  ralsbii  50562