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 2145  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  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  3359  rexcom4b  3488  ceqsrex2v  3620  clel5  3627  reu7  3698  2reu5a  3710  0el  4319  n0snor2el  4794  uni0b  4895  iuncom  4960  iuncom4  4961  iuniin  4965  dfiunv2  4994  iunab  5012  iunid  5021  iunsn  5026  iunn0  5027  iunin2  5031  iundif2  5034  iunun  5055  iunxiun  5059  iunpwss  5069  axrep6OLD  5242  inuni  5311  reusv2lem5  5364  iunopab  5535  dffr2  5613  dffr2ALT  5614  frc  5615  frminex  5631  dfepfr  5636  epfrc  5637  xpiundi  5723  xpiundir  5724  reliin  5795  iunxpf  5825  cnvuni  5867  dmiun  5894  dmopab2rex  5898  elres  6010  elidinxp  6037  dfima3  6056  dffr3  6092  rniun  6136  xpdifid  6157  xpdifcnvepel  6158  dminxp  6170  imaco  6242  coiun  6248  imaindm  6290  dffr4  6311  frpomin2  6332  sucel  6426  isarep1  6614  rexrn  7072  ralrn  7073  elrnrexdmb  7075  fnasrn  7131  ralima  7225  reximaOLD  7227  ralimaOLD  7228  abrexco  7232  imaiun  7233  fliftcnv  7299  imaeqsexvOLD  7351  rexrnmpo  7540  imaeqexov  7638  iunpw  7758  abrexex2g  7949  el2xptp  8020  poxp2  8127  poxp3  8134  soseq  8143  frrlem9  8279  rdglem1  8390  tz7.49  8420  oarec  8535  omeu  8558  qsid  8767  eroveu  8798  ixp0  8917  fimax2g  9234  marypha2lem2  9384  dfsup2  9392  infcllem  9436  dfoi  9461  wemapsolem  9500  zfregcl  9544  zfregclOLD  9545  zfreg  9546  zfregfr  9561  oemapso  9639  brttrcl2  9671  ttrclresv  9674  zfregs2  9690  infenaleph  10063  isinfcard  10064  kmlem7  10128  kmlem13  10134  fin23lem26  10297  dffin1-5  10360  fin12  10385  numth  10444  ac6n  10457  zorn2lem7  10474  zorng  10476  brdom7disj  10503  brdom6disj  10504  uniwun  10713  axgroth5  10797  axgroth4  10805  grothprim  10807  npomex  10969  genpass  10982  elreal  11104  dfinfre  12187  infrenegsup  12189  uzwo  12926  ublbneg  12948  xrinfmss2  13328  4fvwrd4  13667  fsuppmapnn0fiubex  14019  fsuppmapnn0ub  14022  mptnn0fsuppr  14026  hashge2el2dif  14507  cshwsexa  14851  dfrtrclrec2  15085  rexanuz  15387  rexfiuz  15389  clim0  15547  cbvsum  15736  cbvsumv  15737  incexc2  15882  cbvprod  15957  cbvprodv  15958  prodeq1i  15960  fprodle  16040  iprodmul  16047  divalglem10  16450  divalgb  16452  ncoprmlnprm  16777  pythagtriplem2  16867  pythagtriplem19  16883  pythagtrip  16884  pceu  16896  prmreclem6  16971  4sqlem12  17006  cshwshashlem1  17145  cshwshash  17154  imasaddfnlem  17572  isdrs2  18352  chnfi  18680  smndex1mgm  18959  smndex1n0mnd  18964  pmtrprfvalrn  19549  pgpfac1lem5  20142  dvdsrval  20434  opprunit  20450  lsmspsn  21174  lsmelval2  21175  islpidl  21453  pzriprnglem3  21593  pzriprnglem10  21600  mat1dimelbas  22589  mat1dimbas  22590  mdetunilem8  22737  pmatcollpw2lem  22895  tgval2  23074  ntreq0  23195  isclo2  23206  neiptopnei  23250  ist0-3  23463  tgcmp  23519  cmpfi  23526  is1stc2  23560  unisngl  23645  xkobval  23704  txtube  23758  txcmplem1  23759  xkococnlem  23777  eltsms  24251  metrest  24642  iscau3  25398  bcth  25449  pmltpc  25570  itg2i1fseq  25875  itg2cn  25883  plyun0  26315  aaliou3lem9  26472  1cubr  26965  dchrvmasumlema  27622  selbergsb  27697  ostth  27761  noseponlem  27786  nosepon  27787  nolt02o  27817  noinfbnd1lem1  27845  noinfbnd1lem4  27848  cuteq1  27968  elold  28010  made0  28014  lrrecfr  28094  leadds1  28140  addsuniflem  28152  addsasslem1  28154  addsasslem2  28155  mulsrid  28264  mulsuniflem  28300  addsdilem1  28302  addsdilem2  28303  mulsasslem1  28314  mulsasslem2  28315  z12sge0  28634  elreno2  28646  renegscl  28649  istrkg2ld  28687  tglowdim1i  28728  legtrid  28818  midex  28968  ishpg  28990  brbtwn2  29164  colinearalg  29169  ax5seg  29197  axpasch  29200  axlowdimlem6  29206  axeuclidlem  29221  axeuclid  29222  elntg2  29244  umgr2edg1  29470  umgr2edgneu  29473  nbgrsym  29622  isuvtx  29654  usgr2pth0  30023  wlkiswwlksupgr2  30135  clwwlknun  30372  4cycl2vnunb  30550  fusgreg2wsp  30596  lpni  30741  nmobndseqi  31040  hhcmpl  31461  shne0i  31709  nmcopexi  32288  nmcfnexi  32312  cdj3lem3b  32701  rexcom4f  32725  reuxfrdf  32747  iunin1f  32812  ofpreima  32922  intimafv  32968  fpwrelmapffslem  32989  tosglblem  33207  xrnarchi  33417  isunit2  33472  isdrng4  33531  dvdsrspss  33616  lsmsnorb  33620  lsmsnorb2  33621  1arithufdlem4  33754  constrconj  34052  ordtconnlem1  34231  lmdvg  34260  esumfsup  34377  reprsuc  34919  reprdifc  34931  bnj168  35036  bnj1185  35098  bnj1542  35162  bnj865  35228  bnj916  35238  bnj983  35256  bnj1176  35310  bnj1189  35314  bnj1296  35326  bnj1398  35339  bnj1450  35355  bnj1463  35360  nummin  35399  fineqvnttrclse  35432  axregszf  35437  onvf1odlem1  35458  loop1cycl  35500  cvmliftlem15  35661  cvmlift2lem12  35677  satfvsuclem2  35723  satfvsucsuc  35728  satfdm  35732  satf0  35735  dmopab3rexdif  35768  rexxfr3dALT  36002  dffr5  36117  dfon2lem9  36152  brbigcup  36259  elfuns  36276  brimage  36287  brimg  36298  dfrecs2  36313  imagesset  36316  brub  36317  brsegle  36471  sumeq2si  36575  prodeq2si  36577  cbvprodvw2  36620  filnetlem4  36754  bj-rexcom4bv  37379  bj-rexcom4b  37380  bj-elsngl  37465  bj-axseprep  37571  bj-rest10  37590  bj-restreg  37601  bj-mpomptALT  37621  nlpineqsn  37914  fvineqsneq  37918  iundif1  38105  matunitlindflem1  38127  poimirlem1  38132  poimirlem30  38161  poimirlem32  38163  poimir  38164  ismblfin  38172  volsupnfl  38176  itg2addnclem3  38184  fdc  38256  isfldidl  38579  eldmqsres2  38805  n0elqs  38843  rnxrncnvepres  38934  rnxrnidres  38935  dfcoels  39031  br1cossinres  39048  br1cossinidres  39050  br1cossincnvepres  39051  br1cossxrnidres  39052  br1cossxrncnvepres  39053  br1cossxrncnvssrres  39099  eldmqs1cossres  39255  disjdmqscossss  39417  prtlem10  39501  prter2  39517  islshpat  39653  lshpsmreu  39745  2dim  40106  islpln5  40171  lplnexatN  40199  islvol5  40215  dalem18  40317  dalem20  40329  lhpexle2  40646  lhpexle3  40648  lhpex2leN  40649  4atex2  40713  4atex2-0bOLDN  40715  cdlemftr3  41201  cdlemg17pq  41308  cdlemg19  41320  cdlemg21  41322  cdlemg33d  41345  dva1dim  41621  dih1dimatlem  41965  dihglb2  41978  dvh2dim  42081  mapdrvallem2  42281  mapdpglem3  42311  hdmapglem7a  42563  hashnexinjle  42758  aks6d1c5  42768  supinf  42870  fimgmcyclem  43163  dffltz  43228  elrfirn  43288  isnacs2  43299  isnacs3  43303  sbc2rex  43378  4rexfrabdioph  43387  eldioph4b  43400  fphpd  43405  fiphp3d  43408  rencldnfilem  43409  rmxdioph  43605  expdiophlem1  43610  islnm2  43667  onmaxnelsup  43812  onsupnmax  43817  onsupuni  43818  onsupmaxb  43828  tfsconcatlem  43925  tfsconcatrn  43931  oadif1lem  43968  oadif1  43969  elimaint  44237  cnviun  44238  imaiun1  44239  coiun1  44240  elintima  44241  briunov2  44270  clsk3nimkb  44628  expandrexn  44865  prmunb2  44885  zfregs2VD  45414  n0abso  45550  sswfaxreg  45561  evth2f  45593  evthf  45605  ndisj2  45629  rexanuz2nf  46064  fnlimabslt  46251  climbddf  46259  limsupub  46276  limsuppnflem  46282  limsupubuz  46285  limsupre2lem  46296  limsupreuz  46309  limsupvaluz2  46310  cnrefiisplem  46401  cnrefiisp  46402  stoweidlem28  46600  fourierdlem63  46741  fourierdlem65  46743  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem100  46778  sge0pnfmpt  47017  ovn0  47138  smfaddlem1  47335  smflimlem4  47346  fsetsniunop  47641  2rexsb  47693  2rexrsb  47694  cbvrex2  47696  2reu8i  47705  clnbgrsym  48458  isubgr3stgrlem6  48591  copisnmnd  48789  pgrpgt2nabl  48997  islindeps  49084  lindslinindsimp1  49088  lindslinindsimp2  49094  islindeps2  49114  islininds2  49115  isldepslvec2  49116  ldepslinc  49140  sepnsepolem1  49551