Theorem rexbii 3076

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.29imd  3098  r19.43  3101  3r19.43  3102  2rexbii  3109  rexnal2  3115  r19.42v  3169  r19.41vv  3207  3reeanv  3210  cbvrex2vw  3220  rexcom4a  3267  rexcom13  3271  rexrot4  3272  2ex2rexrot  3273  cbvrex2v  3343  rexcom4b  3479  ceqsrex2v  3624  clel5  3631  reu7  3703  2reu5a  3715  0el  4326  n0snor2el  4797  uni0b  4897  iuncom  4963  iuncom4  4964  iuniin  4968  dfiunv2  4999  iunab  5015  iunid  5024  iunsn  5030  iunn0  5031  iunin2  5035  iundif2  5038  iunun  5057  iunxiun  5061  iunpwss  5071  axrep6OLD  5244  inuni  5305  reusv2lem5  5357  iunopab  5519  iunopabOLD  5520  dffr2  5599  dffr2ALT  5600  frc  5601  frminex  5617  dfepfr  5622  epfrc  5623  xpiundi  5709  xpiundir  5710  reliin  5780  iunxpf  5812  cnvuni  5850  dmiun  5877  dmopab2rex  5881  elres  5991  elidinxp  6015  dfima3  6034  dffr3  6070  rniun  6120  xpdifid  6141  dminxp  6153  imaco  6224  coiun  6229  imaindm  6272  dffr4  6293  frpomin2  6314  sucel  6408  isarep1  6606  isarep1OLD  6607  rexrn  7059  ralrn  7060  elrnrexdmb  7062  fnasrn  7117  ralima  7211  reximaOLD  7213  ralimaOLD  7214  abrexco  7218  imaiun  7219  fliftcnv  7286  imaeqsexvOLD  7338  rexrnmpo  7529  imaeqexov  7627  iunpw  7747  abrexex2g  7943  el2xptp  8014  poxp2  8122  poxp3  8129  soseq  8138  frrlem9  8273  rdglem1  8383  tz7.49  8413  oarec  8526  omeu  8549  qsid  8754  eroveu  8785  ixp0  8904  fimax2g  9233  marypha2lem2  9387  dfsup2  9395  infcllem  9439  dfoi  9464  wemapsolem  9503  zfregcl  9547  zfreg  9548  zfregfr  9558  oemapso  9635  brttrcl2  9667  ttrclresv  9670  zfregs2  9686  infenaleph  10044  isinfcard  10045  kmlem7  10110  kmlem13  10116  fin23lem26  10278  dffin1-5  10341  fin12  10366  numth  10425  ac6n  10438  zorn2lem7  10455  zorng  10457  brdom7disj  10484  brdom6disj  10485  uniwun  10693  axgroth5  10777  axgroth4  10785  grothprim  10787  npomex  10949  genpass  10962  elreal  11084  dfinfre  12164  infrenegsup  12166  uzwo  12870  ublbneg  12892  xrinfmss2  13271  4fvwrd4  13609  fsuppmapnn0fiubex  13957  fsuppmapnn0ub  13960  mptnn0fsuppr  13964  hashge2el2dif  14445  cshwsexa  14789  dfrtrclrec2  15024  rexanuz  15312  rexfiuz  15314  clim0  15472  cbvsum  15661  cbvsumv  15662  incexc2  15804  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  fprodle  15962  iprodmul  15969  divalglem10  16372  divalgb  16374  ncoprmlnprm  16698  pythagtriplem2  16788  pythagtriplem19  16804  pythagtrip  16805  pceu  16817  prmreclem6  16892  4sqlem12  16927  cshwshashlem1  17066  cshwshash  17075  imasaddfnlem  17491  isdrs2  18267  smndex1mgm  18834  smndex1n0mnd  18839  pmtrprfvalrn  19418  pgpfac1lem5  20011  dvdsrval  20270  opprunit  20286  lsmspsn  20991  lsmelval2  20992  islpidl  21235  pzriprnglem3  21393  pzriprnglem10  21400  mat1dimelbas  22358  mat1dimbas  22359  mdetunilem8  22506  pmatcollpw2lem  22664  tgval2  22843  ntreq0  22964  isclo2  22975  neiptopnei  23019  ist0-3  23232  tgcmp  23288  cmpfi  23295  is1stc2  23329  unisngl  23414  xkobval  23473  txtube  23527  txcmplem1  23528  xkococnlem  23546  eltsms  24020  metrest  24412  iscau3  25178  bcth  25229  pmltpc  25351  itg2i1fseq  25656  itg2cn  25664  plyun0  26102  aaliou3lem9  26258  1cubr  26752  dchrvmasumlema  27411  selbergsb  27486  ostth  27550  noseponlem  27576  nosepon  27577  nolt02o  27607  noinfbnd1lem1  27635  noinfbnd1lem4  27638  cuteq1  27746  elold  27781  made0  27785  lrrecfr  27850  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  mulsrid  28016  mulsuniflem  28052  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  zs12ge0  28342  renegscl  28349  istrkg2ld  28387  tglowdim1i  28428  legtrid  28518  midex  28664  ishpg  28686  brbtwn2  28832  colinearalg  28837  ax5seg  28865  axpasch  28868  axlowdimlem6  28874  axeuclidlem  28889  axeuclid  28890  elntg2  28912  umgr2edg1  29138  umgr2edgneu  29141  nbgrsym  29290  isuvtx  29322  usgr2pth0  29695  wlkiswwlksupgr2  29807  clwwlknun  30041  4cycl2vnunb  30219  fusgreg2wsp  30265  lpni  30409  nmobndseqi  30708  hhcmpl  31129  shne0i  31377  nmcopexi  31956  nmcfnexi  31980  cdj3lem3b  32369  rexcom4f  32397  reuxfrdf  32420  iunin1f  32486  ofpreima  32589  intimafv  32634  fpwrelmapffslem  32655  tosglblem  32900  xrnarchi  33138  isunit2  33191  isdrng4  33245  dvdsrspss  33358  lsmsnorb  33362  lsmsnorb2  33363  1arithufdlem4  33518  constrconj  33735  ordtconnlem1  33914  lmdvg  33943  esumfsup  34060  reprsuc  34606  reprdifc  34618  bnj168  34720  bnj1185  34783  bnj1542  34847  bnj865  34913  bnj916  34923  bnj983  34941  bnj1176  34995  bnj1189  34999  bnj1296  35011  bnj1398  35024  bnj1450  35040  bnj1463  35045  nummin  35081  onvf1odlem1  35090  loop1cycl  35124  cvmliftlem15  35285  cvmlift2lem12  35301  satfvsuclem2  35347  satfvsucsuc  35352  satfdm  35356  satf0  35359  dmopab3rexdif  35392  rexxfr3dALT  35626  dffr5  35741  dfon2lem9  35779  brbigcup  35886  elfuns  35903  brimage  35914  brimg  35925  dfrecs2  35938  imagesset  35941  brub  35942  brsegle  36096  sumeq2si  36190  prodeq2si  36192  cbvprodvw2  36235  filnetlem4  36369  bj-rexcom4bv  36870  bj-rexcom4b  36871  bj-elsngl  36956  bj-rest10  37076  bj-restreg  37087  bj-mpomptALT  37107  nlpineqsn  37396  fvineqsneq  37400  iundif1  37588  matunitlindflem1  37610  poimirlem1  37615  poimirlem30  37644  poimirlem32  37646  poimir  37647  ismblfin  37655  volsupnfl  37659  itg2addnclem3  37667  fdc  37739  isfldidl  38062  eldmqsres2  38276  n0elqs  38314  rnxrncnvepres  38386  rnxrnidres  38387  dfcoels  38421  br1cossinres  38438  br1cossinidres  38440  br1cossincnvepres  38441  br1cossxrnidres  38442  br1cossxrncnvepres  38443  br1cossxrncnvssrres  38499  eldmqs1cossres  38651  disjdmqscossss  38795  prtlem10  38858  prter2  38874  islshpat  39010  lshpsmreu  39102  2dim  39464  islpln5  39529  lplnexatN  39557  islvol5  39573  dalem18  39675  dalem20  39687  lhpexle2  40004  lhpexle3  40006  lhpex2leN  40007  4atex2  40071  4atex2-0bOLDN  40073  cdlemftr3  40559  cdlemg17pq  40666  cdlemg19  40678  cdlemg21  40680  cdlemg33d  40703  dva1dim  40979  dih1dimatlem  41323  dihglb2  41336  dvh2dim  41439  mapdrvallem2  41639  mapdpglem3  41669  hdmapglem7a  41921  hashnexinjle  42117  aks6d1c5  42127  supinf  42230  fimgmcyclem  42521  dffltz  42622  elrfirn  42683  isnacs2  42694  isnacs3  42698  sbc2rex  42775  4rexfrabdioph  42786  eldioph4b  42799  fphpd  42804  fiphp3d  42807  rencldnfilem  42808  rmxdioph  43005  expdiophlem1  43010  islnm2  43067  onmaxnelsup  43212  onsupnmax  43217  onsupuni  43218  onsupmaxb  43228  tfsconcatlem  43325  tfsconcatrn  43331  oadif1lem  43368  oadif1  43369  elimaint  43638  cnviun  43639  imaiun1  43640  coiun1  43641  elintima  43642  briunov2  43671  clsk3nimkb  44029  expandrexn  44280  prmunb2  44300  zfregs2VD  44830  n0abso  44966  sswfaxreg  44977  evth2f  45009  evthf  45021  ndisj2  45045  rexanuz2nf  45488  fnlimabslt  45677  climbddf  45685  limsupub  45702  limsuppnflem  45708  limsupubuz  45711  limsupre2lem  45722  limsupreuz  45735  limsupvaluz2  45736  cnrefiisplem  45827  cnrefiisp  45828  stoweidlem28  46026  fourierdlem63  46167  fourierdlem65  46169  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem100  46204  sge0pnfmpt  46443  ovn0  46564  smfaddlem1  46761  smflimlem4  46772  fsetsniunop  47050  2rexsb  47102  2rexrsb  47103  cbvrex2  47105  2reu8i  47114  clnbgrsym  47838  isubgr3stgrlem6  47970  copisnmnd  48157  pgrpgt2nabl  48354  islindeps  48442  lindslinindsimp1  48446  lindslinindsimp2  48452  islindeps2  48472  islininds2  48473  isldepslvec2  48474  ldepslinc  48498  sepnsepolem1  48910