Theorem rexbii 3082

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

Syntax hints:   ↔ wb 206   ∈ wcel 2107  ∃wrex 3059

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  r19.29imd  3105  r19.43  3109  2rexbii  3116  rexnal2  3122  r19.42v  3178  r19.41vv  3214  3reeanv  3217  2ralorOLD  3219  cbvrex2vw  3229  rexcomOLD  3276  rexcom4a  3277  rexcom13  3281  rexrot4  3282  2ex2rexrot  3283  cbvrex2v  3353  rexcom4b  3497  ceqsrex2v  3642  clel5  3649  reu7  3722  2reu5a  3734  0el  4345  n0snor2el  4815  uni0b  4915  iuncom  4981  iuncom4  4982  iuniin  4986  dfiunv2  5017  iunab  5033  iunid  5042  iunsn  5048  iunn0  5049  iunin2  5053  iundif2  5056  iunun  5075  iunxiun  5079  iunpwss  5089  axrep6OLD  5271  inuni  5332  reusv2lem5  5384  iunopab  5546  iunopabOLD  5547  dffr2  5628  dffr2ALT  5629  frc  5630  frminex  5646  dfepfr  5651  epfrc  5652  xpiundi  5738  xpiundir  5739  reliin  5809  iunxpf  5841  cnvuni  5879  dmiun  5906  dmopab2rex  5910  elres  6020  elidinxp  6044  dfima3  6063  dffr3  6099  rniun  6149  xpdifid  6170  dminxp  6182  imaco  6253  coiun  6258  imaindm  6301  dffr4  6322  frpomin2  6343  tz6.26OLD  6350  sucel  6439  isarep1  6637  isarep1OLD  6638  rexrn  7088  ralrn  7089  elrnrexdmb  7091  fnasrn  7146  ralima  7240  reximaOLD  7242  ralimaOLD  7243  abrexco  7247  imaiun  7248  fliftcnv  7314  imaeqsexvOLD  7366  rexrnmpo  7556  imaeqexov  7654  iunpw  7774  abrexex2g  7972  el2xptp  8043  poxp2  8151  poxp3  8158  soseq  8167  frrlem9  8302  rdglem1  8438  tz7.49  8468  oarec  8583  omeu  8606  qsid  8806  eroveu  8835  ixp0  8954  fimax2g  9305  marypha2lem2  9459  dfsup2  9467  infcllem  9510  dfoi  9534  wemapsolem  9573  zfregcl  9617  zfreg  9618  zfregfr  9628  oemapso  9705  brttrcl2  9737  ttrclresv  9740  zfregs2  9756  infenaleph  10114  isinfcard  10115  kmlem7  10180  kmlem13  10186  fin23lem26  10348  dffin1-5  10411  fin12  10436  numth  10495  ac6n  10508  zorn2lem7  10525  zorng  10527  brdom7disj  10554  brdom6disj  10555  uniwun  10763  axgroth5  10847  axgroth4  10855  grothprim  10857  npomex  11019  genpass  11032  elreal  11154  dfinfre  12232  infrenegsup  12234  uzwo  12936  ublbneg  12958  xrinfmss2  13336  4fvwrd4  13671  fsuppmapnn0fiubex  14016  fsuppmapnn0ub  14019  mptnn0fsuppr  14023  hashge2el2dif  14502  cshwsexa  14845  dfrtrclrec2  15080  rexanuz  15367  rexfiuz  15369  clim0  15525  cbvsum  15714  cbvsumv  15715  incexc2  15857  cbvprod  15932  cbvprodv  15933  prodeq1i  15935  fprodle  16015  iprodmul  16022  divalglem10  16422  divalgb  16424  ncoprmlnprm  16748  pythagtriplem2  16838  pythagtriplem19  16854  pythagtrip  16855  pceu  16867  prmreclem6  16942  4sqlem12  16977  cshwshashlem1  17116  cshwshash  17125  imasaddfnlem  17549  isdrs2  18327  smndex1mgm  18894  smndex1n0mnd  18899  pmtrprfvalrn  19479  pgpfac1lem5  20072  dvdsrval  20334  opprunit  20350  lsmspsn  21056  lsmelval2  21057  islpidl  21302  pzriprnglem3  21461  pzriprnglem10  21468  mat1dimelbas  22444  mat1dimbas  22445  mdetunilem8  22592  pmatcollpw2lem  22750  tgval2  22929  ntreq0  23050  isclo2  23061  neiptopnei  23105  ist0-3  23318  tgcmp  23374  cmpfi  23381  is1stc2  23415  unisngl  23500  xkobval  23559  txtube  23613  txcmplem1  23614  xkococnlem  23632  eltsms  24106  metrest  24500  iscau3  25267  bcth  25318  pmltpc  25440  itg2i1fseq  25745  itg2cn  25753  plyun0  26191  aaliou3lem9  26347  1cubr  26840  dchrvmasumlema  27499  selbergsb  27574  ostth  27638  noseponlem  27664  nosepon  27665  nolt02o  27695  noinfbnd1lem1  27723  noinfbnd1lem4  27726  cuteq1  27833  elold  27863  made0  27867  lrrecfr  27931  sleadd1  27977  addsuniflem  27989  addsasslem1  27991  addsasslem2  27992  mulsrid  28094  mulsuniflem  28130  addsdilem1  28132  addsdilem2  28133  mulsasslem1  28144  mulsasslem2  28145  renegscl  28385  istrkg2ld  28423  tglowdim1i  28464  legtrid  28554  midex  28700  ishpg  28722  brbtwn2  28869  colinearalg  28874  ax5seg  28902  axpasch  28905  axlowdimlem6  28911  axeuclidlem  28926  axeuclid  28927  elntg2  28949  umgr2edg1  29175  umgr2edgneu  29178  nbgrsym  29327  isuvtx  29359  usgr2pth0  29732  wlkiswwlksupgr2  29844  clwwlknun  30078  4cycl2vnunb  30256  fusgreg2wsp  30302  lpni  30446  nmobndseqi  30745  hhcmpl  31166  shne0i  31414  nmcopexi  31993  nmcfnexi  32017  cdj3lem3b  32406  rexcom4f  32434  reuxfrdf  32457  iunin1f  32517  ofpreima  32622  intimafv  32667  fpwrelmapffslem  32690  tosglblem  32910  xrnarchi  33137  isunit2  33190  isdrng4  33244  dvdsrspss  33356  lsmsnorb  33360  lsmsnorb2  33361  1arithufdlem4  33516  constrconj  33727  ordtconnlem1  33864  lmdvg  33893  esumfsup  34012  reprsuc  34571  reprdifc  34583  bnj168  34685  bnj1185  34748  bnj1542  34812  bnj865  34878  bnj916  34888  bnj983  34906  bnj1176  34960  bnj1189  34964  bnj1296  34976  bnj1398  34989  bnj1450  35005  bnj1463  35010  nummin  35046  loop1cycl  35083  cvmliftlem15  35244  cvmlift2lem12  35260  satfvsuclem2  35306  satfvsucsuc  35311  satfdm  35315  satf0  35318  dmopab3rexdif  35351  rexxfr3dALT  35585  dffr5  35695  dfon2lem9  35733  brbigcup  35840  elfuns  35857  brimage  35868  brimg  35879  dfrecs2  35892  imagesset  35895  brub  35896  brsegle  36050  sumeq2si  36144  prodeq2si  36146  cbvprodvw2  36189  filnetlem4  36323  bj-rexcom4bv  36824  bj-rexcom4b  36825  bj-elsngl  36910  bj-rest10  37030  bj-restreg  37041  bj-mpomptALT  37061  nlpineqsn  37350  fvineqsneq  37354  iundif1  37542  matunitlindflem1  37564  poimirlem1  37569  poimirlem30  37598  poimirlem32  37600  poimir  37601  ismblfin  37609  volsupnfl  37613  itg2addnclem3  37621  fdc  37693  isfldidl  38016  eldmqsres2  38230  n0elqs  38268  rnxrncnvepres  38342  rnxrnidres  38343  dfcoels  38372  br1cossinres  38389  br1cossinidres  38391  br1cossincnvepres  38392  br1cossxrnidres  38393  br1cossxrncnvepres  38394  br1cossxrncnvssrres  38450  eldmqs1cossres  38601  disjdmqscossss  38745  prtlem10  38807  prter2  38823  islshpat  38959  lshpsmreu  39051  2dim  39413  islpln5  39478  lplnexatN  39506  islvol5  39522  dalem18  39624  dalem20  39636  lhpexle2  39953  lhpexle3  39955  lhpex2leN  39956  4atex2  40020  4atex2-0bOLDN  40022  cdlemftr3  40508  cdlemg17pq  40615  cdlemg19  40627  cdlemg21  40629  cdlemg33d  40652  dva1dim  40928  dih1dimatlem  41272  dihglb2  41285  dvh2dim  41388  mapdrvallem2  41588  mapdpglem3  41618  hdmapglem7a  41870  hashnexinjle  42071  aks6d1c5  42081  supinf  42223  fimgmcyclem  42488  dffltz  42589  elrfirn  42651  isnacs2  42662  isnacs3  42666  sbc2rex  42743  4rexfrabdioph  42754  eldioph4b  42767  fphpd  42772  fiphp3d  42775  rencldnfilem  42776  rmxdioph  42973  expdiophlem1  42978  islnm2  43035  onmaxnelsup  43180  onsupnmax  43185  onsupuni  43186  onsupmaxb  43196  tfsconcatlem  43294  tfsconcatrn  43300  oadif1lem  43337  oadif1  43338  elimaint  43607  cnviun  43608  imaiun1  43609  coiun1  43610  elintima  43611  briunov2  43640  clsk3nimkb  43998  expandrexn  44255  prmunb2  44275  zfregs2VD  44806  n0abso  44938  sswfaxreg  44949  evth2f  44965  evthf  44977  ndisj2  45001  rexanuz2nf  45448  fnlimabslt  45639  climbddf  45647  limsupub  45664  limsuppnflem  45670  limsupubuz  45673  limsupre2lem  45684  limsupreuz  45697  limsupvaluz2  45698  cnrefiisplem  45789  cnrefiisp  45790  stoweidlem28  45988  fourierdlem63  46129  fourierdlem65  46131  fourierdlem89  46155  fourierdlem90  46156  fourierdlem91  46157  fourierdlem100  46166  sge0pnfmpt  46405  ovn0  46526  smfaddlem1  46723  smflimlem4  46734  fsetsniunop  47007  2rexsb  47059  2rexrsb  47060  cbvrex2  47062  2reu8i  47071  clnbgrsym  47770  isubgr3stgrlem6  47884  copisnmnd  48031  pgrpgt2nabl  48228  islindeps  48316  lindslinindsimp1  48320  lindslinindsimp2  48326  islindeps2  48346  islininds2  48347  isldepslvec2  48348  ldepslinc  48372  sepnsepolem1  48767