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  3094  r19.43  3097  3r19.43  3098  2rexbii  3105  rexnal2  3111  r19.42v  3161  r19.41vv  3199  3reeanv  3202  cbvrex2vw  3212  rexcom4a  3259  rexcom13  3263  rexrot4  3264  2ex2rexrot  3265  cbvrex2v  3334  rexcom4b  3470  ceqsrex2v  3615  clel5  3622  reu7  3694  2reu5a  3706  0el  4316  n0snor2el  4787  uni0b  4887  iuncom  4952  iuncom4  4953  iuniin  4957  dfiunv2  4987  iunab  5003  iunid  5012  iunsn  5018  iunn0  5019  iunin2  5023  iundif2  5026  iunun  5045  iunxiun  5049  iunpwss  5059  axrep6OLD  5231  inuni  5292  reusv2lem5  5344  iunopab  5506  dffr2  5584  dffr2ALT  5585  frc  5586  frminex  5602  dfepfr  5607  epfrc  5608  xpiundi  5694  xpiundir  5695  reliin  5764  iunxpf  5795  cnvuni  5833  dmiun  5860  dmopab2rex  5864  elres  5975  elidinxp  5999  dfima3  6018  dffr3  6054  rniun  6100  xpdifid  6121  dminxp  6133  imaco  6204  coiun  6209  imaindm  6251  dffr4  6272  frpomin2  6293  sucel  6387  isarep1  6575  rexrn  7025  ralrn  7026  elrnrexdmb  7028  fnasrn  7083  ralima  7177  reximaOLD  7179  ralimaOLD  7180  abrexco  7184  imaiun  7185  fliftcnv  7252  imaeqsexvOLD  7304  rexrnmpo  7493  imaeqexov  7591  iunpw  7711  abrexex2g  7906  el2xptp  7977  poxp2  8083  poxp3  8090  soseq  8099  frrlem9  8234  rdglem1  8344  tz7.49  8374  oarec  8487  omeu  8510  qsid  8715  eroveu  8746  ixp0  8865  fimax2g  9191  marypha2lem2  9345  dfsup2  9353  infcllem  9397  dfoi  9422  wemapsolem  9461  zfregcl  9505  zfregclOLD  9506  zfreg  9507  zfregfr  9519  oemapso  9597  brttrcl2  9629  ttrclresv  9632  zfregs2  9648  infenaleph  10004  isinfcard  10005  kmlem7  10070  kmlem13  10076  fin23lem26  10238  dffin1-5  10301  fin12  10326  numth  10385  ac6n  10398  zorn2lem7  10415  zorng  10417  brdom7disj  10444  brdom6disj  10445  uniwun  10653  axgroth5  10737  axgroth4  10745  grothprim  10747  npomex  10909  genpass  10922  elreal  11044  dfinfre  12124  infrenegsup  12126  uzwo  12830  ublbneg  12852  xrinfmss2  13231  4fvwrd4  13569  fsuppmapnn0fiubex  13917  fsuppmapnn0ub  13920  mptnn0fsuppr  13924  hashge2el2dif  14405  cshwsexa  14748  dfrtrclrec2  14983  rexanuz  15271  rexfiuz  15273  clim0  15431  cbvsum  15620  cbvsumv  15621  incexc2  15763  cbvprod  15838  cbvprodv  15839  prodeq1i  15841  fprodle  15921  iprodmul  15928  divalglem10  16331  divalgb  16333  ncoprmlnprm  16657  pythagtriplem2  16747  pythagtriplem19  16763  pythagtrip  16764  pceu  16776  prmreclem6  16851  4sqlem12  16886  cshwshashlem1  17025  cshwshash  17034  imasaddfnlem  17450  isdrs2  18230  smndex1mgm  18799  smndex1n0mnd  18804  pmtrprfvalrn  19385  pgpfac1lem5  19978  dvdsrval  20264  opprunit  20280  lsmspsn  21006  lsmelval2  21007  islpidl  21250  pzriprnglem3  21408  pzriprnglem10  21415  mat1dimelbas  22374  mat1dimbas  22375  mdetunilem8  22522  pmatcollpw2lem  22680  tgval2  22859  ntreq0  22980  isclo2  22991  neiptopnei  23035  ist0-3  23248  tgcmp  23304  cmpfi  23311  is1stc2  23345  unisngl  23430  xkobval  23489  txtube  23543  txcmplem1  23544  xkococnlem  23562  eltsms  24036  metrest  24428  iscau3  25194  bcth  25245  pmltpc  25367  itg2i1fseq  25672  itg2cn  25680  plyun0  26118  aaliou3lem9  26274  1cubr  26768  dchrvmasumlema  27427  selbergsb  27502  ostth  27566  noseponlem  27592  nosepon  27593  nolt02o  27623  noinfbnd1lem1  27651  noinfbnd1lem4  27654  cuteq1  27766  elold  27801  made0  27805  lrrecfr  27873  sleadd1  27919  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  mulsrid  28039  mulsuniflem  28075  addsdilem1  28077  addsdilem2  28078  mulsasslem1  28089  mulsasslem2  28090  zs12ge0  28378  renegscl  28385  istrkg2ld  28423  tglowdim1i  28464  legtrid  28554  midex  28700  ishpg  28722  brbtwn2  28868  colinearalg  28873  ax5seg  28901  axpasch  28904  axlowdimlem6  28910  axeuclidlem  28925  axeuclid  28926  elntg2  28948  umgr2edg1  29174  umgr2edgneu  29177  nbgrsym  29326  isuvtx  29358  usgr2pth0  29728  wlkiswwlksupgr2  29840  clwwlknun  30074  4cycl2vnunb  30252  fusgreg2wsp  30298  lpni  30442  nmobndseqi  30741  hhcmpl  31162  shne0i  31410  nmcopexi  31989  nmcfnexi  32013  cdj3lem3b  32402  rexcom4f  32430  reuxfrdf  32453  iunin1f  32519  ofpreima  32622  intimafv  32667  fpwrelmapffslem  32688  tosglblem  32929  xrnarchi  33136  isunit2  33190  isdrng4  33244  dvdsrspss  33334  lsmsnorb  33338  lsmsnorb2  33339  1arithufdlem4  33494  constrconj  33711  ordtconnlem1  33890  lmdvg  33919  esumfsup  34036  reprsuc  34582  reprdifc  34594  bnj168  34696  bnj1185  34759  bnj1542  34823  bnj865  34889  bnj916  34899  bnj983  34917  bnj1176  34971  bnj1189  34975  bnj1296  34987  bnj1398  35000  bnj1450  35016  bnj1463  35021  nummin  35057  axregszf  35063  onvf1odlem1  35075  loop1cycl  35109  cvmliftlem15  35270  cvmlift2lem12  35286  satfvsuclem2  35332  satfvsucsuc  35337  satfdm  35341  satf0  35344  dmopab3rexdif  35377  rexxfr3dALT  35611  dffr5  35726  dfon2lem9  35764  brbigcup  35871  elfuns  35888  brimage  35899  brimg  35910  dfrecs2  35923  imagesset  35926  brub  35927  brsegle  36081  sumeq2si  36175  prodeq2si  36177  cbvprodvw2  36220  filnetlem4  36354  bj-rexcom4bv  36855  bj-rexcom4b  36856  bj-elsngl  36941  bj-rest10  37061  bj-restreg  37072  bj-mpomptALT  37092  nlpineqsn  37381  fvineqsneq  37385  iundif1  37573  matunitlindflem1  37595  poimirlem1  37600  poimirlem30  37629  poimirlem32  37631  poimir  37632  ismblfin  37640  volsupnfl  37644  itg2addnclem3  37652  fdc  37724  isfldidl  38047  eldmqsres2  38261  n0elqs  38299  rnxrncnvepres  38371  rnxrnidres  38372  dfcoels  38406  br1cossinres  38423  br1cossinidres  38425  br1cossincnvepres  38426  br1cossxrnidres  38427  br1cossxrncnvepres  38428  br1cossxrncnvssrres  38484  eldmqs1cossres  38636  disjdmqscossss  38780  prtlem10  38843  prter2  38859  islshpat  38995  lshpsmreu  39087  2dim  39449  islpln5  39514  lplnexatN  39542  islvol5  39558  dalem18  39660  dalem20  39672  lhpexle2  39989  lhpexle3  39991  lhpex2leN  39992  4atex2  40056  4atex2-0bOLDN  40058  cdlemftr3  40544  cdlemg17pq  40651  cdlemg19  40663  cdlemg21  40665  cdlemg33d  40688  dva1dim  40964  dih1dimatlem  41308  dihglb2  41321  dvh2dim  41424  mapdrvallem2  41624  mapdpglem3  41654  hdmapglem7a  41906  hashnexinjle  42102  aks6d1c5  42112  supinf  42215  fimgmcyclem  42506  dffltz  42607  elrfirn  42668  isnacs2  42679  isnacs3  42683  sbc2rex  42760  4rexfrabdioph  42771  eldioph4b  42784  fphpd  42789  fiphp3d  42792  rencldnfilem  42793  rmxdioph  42989  expdiophlem1  42994  islnm2  43051  onmaxnelsup  43196  onsupnmax  43201  onsupuni  43202  onsupmaxb  43212  tfsconcatlem  43309  tfsconcatrn  43315  oadif1lem  43352  oadif1  43353  elimaint  43622  cnviun  43623  imaiun1  43624  coiun1  43625  elintima  43626  briunov2  43655  clsk3nimkb  44013  expandrexn  44264  prmunb2  44284  zfregs2VD  44814  n0abso  44950  sswfaxreg  44961  evth2f  44993  evthf  45005  ndisj2  45029  rexanuz2nf  45472  fnlimabslt  45661  climbddf  45669  limsupub  45686  limsuppnflem  45692  limsupubuz  45695  limsupre2lem  45706  limsupreuz  45719  limsupvaluz2  45720  cnrefiisplem  45811  cnrefiisp  45812  stoweidlem28  46010  fourierdlem63  46151  fourierdlem65  46153  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem100  46188  sge0pnfmpt  46427  ovn0  46548  smfaddlem1  46745  smflimlem4  46756  fsetsniunop  47034  2rexsb  47086  2rexrsb  47087  cbvrex2  47089  2reu8i  47098  clnbgrsym  47823  isubgr3stgrlem6  47956  copisnmnd  48154  pgrpgt2nabl  48351  islindeps  48439  lindslinindsimp1  48443  lindslinindsimp2  48449  islindeps2  48469  islininds2  48470  isldepslvec2  48471  ldepslinc  48495  sepnsepolem1  48907