Theorem rexbii 3093

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

Syntax hints:   ↔ wb 205   ∈ wcel 2105  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  r19.29imd  3117  r19.43  3121  2rexbii  3128  rexnal2  3134  r19.42v  3189  r19.41vv  3223  3reeanv  3226  2ralorOLD  3228  cbvrex2vw  3238  rexcomOLD  3287  rexcom4a  3288  rexcom13  3292  rexrot4  3293  2ex2rexrot  3294  cbvrex2v  3364  rexcom4b  3503  ceqsrex2v  3646  clel5  3655  reu7  3728  2reu5a  3740  0el  4360  n0snor2el  4834  uni0b  4937  iuncom  5004  iuncom4  5005  iuniin  5009  dfiunv2  5038  iunab  5054  iunid  5063  iunsn  5069  iunn0  5070  iunin2  5074  iundif2  5077  iunun  5096  iunxiun  5100  iunpwss  5110  axrep6  5292  inuni  5343  reusv2lem5  5400  iunopab  5559  iunopabOLD  5560  dffr2  5640  dffr2ALT  5641  frc  5642  frminex  5656  dfepfr  5661  epfrc  5662  xpiundi  5746  xpiundir  5747  reliin  5817  iunxpf  5848  cnvuni  5886  dmiun  5913  dmopab2rex  5917  elres  6020  elidinxp  6043  dfima3  6062  dffr3  6098  rniun  6147  xpdifid  6167  dminxp  6179  imaco  6250  coiun  6255  imaindm  6298  dffr4  6320  frpomin2  6342  tz6.26OLD  6349  sucel  6438  isarep1  6637  isarep1OLD  6638  rexrn  7088  ralrn  7089  elrnrexdmb  7091  fnasrn  7145  rexima  7241  ralima  7242  abrexco  7246  imaiun  7247  fliftcnv  7311  imaeqsexv  7363  rexrnmpo  7551  imaeqexov  7649  iunpw  7762  abrexex2g  7955  el2xptp  8025  poxp2  8134  poxp3  8141  soseq  8150  frrlem9  8285  rdglem1  8421  tz7.49  8451  oarec  8568  omeu  8591  qsid  8783  eroveu  8812  ixp0  8931  fimax2g  9295  marypha2lem2  9437  dfsup2  9445  infcllem  9488  dfoi  9512  wemapsolem  9551  zfregcl  9595  zfreg  9596  zfregfr  9606  oemapso  9683  brttrcl2  9715  ttrclresv  9718  zfregs2  9734  infenaleph  10092  isinfcard  10093  kmlem7  10157  kmlem13  10163  fin23lem26  10326  dffin1-5  10389  fin12  10414  numth  10473  ac6n  10486  zorn2lem7  10503  zorng  10505  brdom7disj  10532  brdom6disj  10533  uniwun  10741  axgroth5  10825  axgroth4  10833  grothprim  10835  npomex  10997  genpass  11010  elreal  11132  dfinfre  12202  infrenegsup  12204  uzwo  12902  ublbneg  12924  xrinfmss2  13297  4fvwrd4  13628  fsuppmapnn0fiubex  13964  fsuppmapnn0ub  13967  mptnn0fsuppr  13971  hashge2el2dif  14448  cshwsexa  14781  dfrtrclrec2  15012  rexanuz  15299  rexfiuz  15301  clim0  15457  cbvsum  15648  incexc2  15791  cbvprod  15866  fprodle  15947  iprodmul  15954  divalglem10  16352  divalgb  16354  ncoprmlnprm  16671  pythagtriplem2  16757  pythagtriplem19  16773  pythagtrip  16774  pceu  16786  prmreclem6  16861  4sqlem12  16896  cshwshashlem1  17036  cshwshash  17045  imasaddfnlem  17481  isdrs2  18269  smndex1mgm  18830  smndex1n0mnd  18835  pmtrprfvalrn  19404  pgpfac1lem5  19997  dvdsrval  20259  opprunit  20275  lsmspsn  20928  lsmelval2  20929  islpidl  21173  pzriprnglem3  21343  pzriprnglem10  21350  mat1dimelbas  22293  mat1dimbas  22294  mdetunilem8  22441  pmatcollpw2lem  22599  tgval2  22779  ntreq0  22901  isclo2  22912  neiptopnei  22956  ist0-3  23169  tgcmp  23225  cmpfi  23232  is1stc2  23266  unisngl  23351  xkobval  23410  txtube  23464  txcmplem1  23465  xkococnlem  23483  eltsms  23957  metrest  24353  iscau3  25126  bcth  25177  pmltpc  25299  itg2i1fseq  25605  itg2cn  25613  plyun0  26049  aaliou3lem9  26202  1cubr  26688  dchrvmasumlema  27346  selbergsb  27421  ostth  27485  noseponlem  27510  nosepon  27511  nolt02o  27541  noinfbnd1lem1  27569  noinfbnd1lem4  27572  cuteq1  27679  elold  27709  made0  27713  lrrecfr  27773  sleadd1  27819  addsuniflem  27831  addsasslem1  27833  addsasslem2  27834  mulsrid  27926  mulsuniflem  27962  addsdilem1  27964  addsdilem2  27965  mulsasslem1  27976  mulsasslem2  27977  renegscl  28106  istrkg2ld  28144  tglowdim1i  28185  legtrid  28275  midex  28421  ishpg  28443  brbtwn2  28596  colinearalg  28601  ax5seg  28629  axpasch  28632  axlowdimlem6  28638  axeuclidlem  28653  axeuclid  28654  elntg2  28676  umgr2edg1  28901  umgr2edgneu  28904  nbgrsym  29053  isuvtx  29085  usgr2pth0  29455  wlkiswwlksupgr2  29564  clwwlknun  29798  4cycl2vnunb  29976  fusgreg2wsp  30022  lpni  30166  nmobndseqi  30465  hhcmpl  30886  shne0i  31134  nmcopexi  31713  nmcfnexi  31737  cdj3lem3b  32126  rexcom4f  32143  reuxfrdf  32164  iunin1f  32222  ofpreima  32323  intimafv  32365  fpwrelmapffslem  32390  tosglblem  32577  xrnarchi  32766  isdrng4  32831  dvdsrspss  32931  lsmsnorb  32941  lsmsnorb2  32942  ordtconnlem1  33368  lmdvg  33397  esumfsup  33532  reprsuc  34091  reprdifc  34103  bnj168  34205  bnj1185  34268  bnj1542  34332  bnj865  34398  bnj916  34408  bnj983  34426  bnj1176  34480  bnj1189  34484  bnj1296  34496  bnj1398  34509  bnj1450  34525  bnj1463  34530  nummin  34558  loop1cycl  34592  cvmliftlem15  34753  cvmlift2lem12  34769  satfvsuclem2  34815  satfvsucsuc  34820  satfdm  34824  satf0  34827  dmopab3rexdif  34860  dffr5  35194  dfon2lem9  35233  brbigcup  35340  elfuns  35357  brimage  35368  brimg  35379  dfrecs2  35392  imagesset  35395  brub  35396  brsegle  35550  filnetlem4  35730  bj-rexcom4bv  36226  bj-rexcom4b  36227  bj-elsngl  36313  bj-rest10  36433  bj-restreg  36444  bj-mpomptALT  36464  nlpineqsn  36753  fvineqsneq  36757  iundif1  36926  matunitlindflem1  36948  poimirlem1  36953  poimirlem30  36982  poimirlem32  36984  poimir  36985  ismblfin  36993  volsupnfl  36997  itg2addnclem3  37005  fdc  37077  isfldidl  37400  eldmqsres2  37620  n0elqs  37659  rnxrncnvepres  37734  rnxrnidres  37735  dfcoels  37764  br1cossinres  37781  br1cossinidres  37783  br1cossincnvepres  37784  br1cossxrnidres  37785  br1cossxrncnvepres  37786  br1cossxrncnvssrres  37842  eldmqs1cossres  37993  disjdmqscossss  38137  prtlem10  38199  prter2  38215  islshpat  38351  lshpsmreu  38443  2dim  38805  islpln5  38870  lplnexatN  38898  islvol5  38914  dalem18  39016  dalem20  39028  lhpexle2  39345  lhpexle3  39347  lhpex2leN  39348  4atex2  39412  4atex2-0bOLDN  39414  cdlemftr3  39900  cdlemg17pq  40007  cdlemg19  40019  cdlemg21  40021  cdlemg33d  40044  dva1dim  40320  dih1dimatlem  40664  dihglb2  40677  dvh2dim  40780  mapdrvallem2  40980  mapdpglem3  41010  hdmapglem7a  41262  dffltz  41839  elrfirn  41896  isnacs2  41907  isnacs3  41911  sbc2rex  41988  4rexfrabdioph  41999  eldioph4b  42012  fphpd  42017  fiphp3d  42020  rencldnfilem  42021  rmxdioph  42218  expdiophlem1  42223  islnm2  42283  onmaxnelsup  42435  onsupnmax  42440  onsupuni  42441  onsupmaxb  42451  tfsconcatlem  42549  tfsconcatrn  42555  oadif1lem  42592  oadif1  42593  elimaint  42863  cnviun  42864  imaiun1  42865  coiun1  42866  elintima  42867  briunov2  42896  clsk3nimkb  43254  expandrexn  43513  prmunb2  43533  zfregs2VD  44065  evth2f  44162  evthf  44174  ndisj2  44200  rexanuz2nf  44662  fnlimabslt  44854  climbddf  44862  limsupub  44879  limsuppnflem  44885  limsupubuz  44888  limsupre2lem  44899  limsupreuz  44912  limsupvaluz2  44913  cnrefiisplem  45004  cnrefiisp  45005  stoweidlem28  45203  fourierdlem63  45344  fourierdlem65  45346  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  fourierdlem100  45381  sge0pnfmpt  45620  ovn0  45741  smfaddlem1  45938  smflimlem4  45949  fsetsniunop  46218  2rexsb  46268  2rexrsb  46269  cbvrex2  46271  2reu8i  46280  copisnmnd  47006  pgrpgt2nabl  47205  islindeps  47296  lindslinindsimp1  47300  lindslinindsimp2  47306  islindeps2  47326  islininds2  47327  isldepslvec2  47328  ldepslinc  47352  sepnsepolem1  47716