Theorem rexbii 3118

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149  ∃wrex 3095

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  r19.29imd  3136  r19.43  3139  3r19.43  3140  2rexbii  3147  rexnal2  3153  r19.42v  3203  r19.41vv  3241  3reeanv  3244  cbvrex2vw  3254  rexcom4a  3301  rexcom13  3304  rexrot4  3305  2ex2rexrot  3306  cbvrex2v  3365  rexcom4b  3494  ceqsrex2v  3626  clel5  3633  reu7  3704  2reu5a  3716  0el  4325  n0snor2el  4799  uni0b  4900  iuncom  4965  iuncom4  4966  iuniin  4970  dfiunv2  4999  iunab  5017  iunid  5026  iunsn  5031  iunn0  5032  iunin2  5036  iundif2  5039  iunun  5060  iunxiun  5064  iunpwss  5074  axrep6OLD  5249  inuni  5318  reusv2lem5  5371  iunopab  5542  dffr2  5620  dffr2ALT  5621  frc  5622  frminex  5638  dfepfr  5643  epfrc  5644  xpiundi  5730  xpiundir  5731  reliin  5802  iunxpf  5832  cnvuni  5874  dmiun  5901  dmopab2rex  5905  elres  6017  elidinxp  6044  dfima3  6063  dffr3  6099  rniun  6143  xpdifid  6164  xpdifcnvepel  6165  dminxp  6177  imaco  6249  coiun  6255  imaindm  6297  dffr4  6318  frpomin2  6339  sucel  6434  isarep1  6622  rexrn  7080  ralrn  7081  elrnrexdmb  7083  fnasrn  7139  ralima  7233  reximaOLD  7235  ralimaOLD  7236  abrexco  7240  imaiun  7241  fliftcnv  7307  imaeqsexvOLD  7359  rexrnmpo  7548  imaeqexov  7646  iunpw  7766  abrexex2g  7957  el2xptp  8028  poxp2  8135  poxp3  8142  soseq  8151  frrlem9  8287  rdglem1  8398  tz7.49  8428  oarec  8543  omeu  8566  qsid  8775  eroveu  8806  ixp0  8925  fimax2g  9242  marypha2lem2  9392  dfsup2  9400  infcllem  9444  dfoi  9469  wemapsolem  9508  zfregcl  9552  zfregclOLD  9553  zfreg  9554  zfregfr  9569  oemapso  9647  brttrcl2  9679  ttrclresv  9682  zfregs2  9698  infenaleph  10071  isinfcard  10072  kmlem7  10136  kmlem13  10142  fin23lem26  10305  dffin1-5  10368  fin12  10393  numth  10452  ac6n  10465  zorn2lem7  10482  zorng  10484  brdom7disj  10511  brdom6disj  10512  uniwun  10721  axgroth5  10805  axgroth4  10813  grothprim  10815  npomex  10977  genpass  10990  elreal  11112  dfinfre  12192  infrenegsup  12194  uzwo  12931  ublbneg  12953  xrinfmss2  13333  4fvwrd4  13672  fsuppmapnn0fiubex  14024  fsuppmapnn0ub  14027  mptnn0fsuppr  14031  hashge2el2dif  14513  cshwsexa  14857  dfrtrclrec2  15091  rexanuz  15393  rexfiuz  15395  clim0  15553  cbvsum  15742  cbvsumv  15743  incexc2  15888  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  fprodle  16046  iprodmul  16053  divalglem10  16456  divalgb  16458  ncoprmlnprm  16783  pythagtriplem2  16873  pythagtriplem19  16889  pythagtrip  16890  pceu  16902  prmreclem6  16977  4sqlem12  17012  cshwshashlem1  17151  cshwshash  17160  imasaddfnlem  17578  isdrs2  18358  chnfi  18686  smndex1mgm  18965  smndex1n0mnd  18970  pmtrprfvalrn  19554  pgpfac1lem5  20147  dvdsrval  20439  opprunit  20455  lsmspsn  21179  lsmelval2  21180  islpidl  21458  pzriprnglem3  21598  pzriprnglem10  21605  mat1dimelbas  22593  mat1dimbas  22594  mdetunilem8  22741  pmatcollpw2lem  22899  tgval2  23078  ntreq0  23199  isclo2  23210  neiptopnei  23254  ist0-3  23467  tgcmp  23523  cmpfi  23530  is1stc2  23564  unisngl  23649  xkobval  23708  txtube  23762  txcmplem1  23763  xkococnlem  23781  eltsms  24255  metrest  24646  iscau3  25402  bcth  25453  pmltpc  25574  itg2i1fseq  25879  itg2cn  25887  plyun0  26319  aaliou3lem9  26476  1cubr  26969  dchrvmasumlema  27626  selbergsb  27701  ostth  27765  noseponlem  27790  nosepon  27791  nolt02o  27821  noinfbnd1lem1  27849  noinfbnd1lem4  27852  cuteq1  27972  elold  28014  made0  28018  lrrecfr  28098  leadds1  28144  addsuniflem  28156  addsasslem1  28158  addsasslem2  28159  mulsrid  28268  mulsuniflem  28304  addsdilem1  28306  addsdilem2  28307  mulsasslem1  28318  mulsasslem2  28319  z12sge0  28638  elreno2  28650  renegscl  28653  istrkg2ld  28691  tglowdim1i  28732  legtrid  28822  midex  28973  ishpg  28996  brbtwn2  29192  colinearalg  29197  ax5seg  29225  axpasch  29228  axlowdimlem6  29234  axeuclidlem  29249  axeuclid  29250  elntg2  29272  umgr2edg1  29498  umgr2edgneu  29501  nbgrsym  29650  isuvtx  29682  usgr2pth0  30051  wlkiswwlksupgr2  30163  clwwlknun  30400  4cycl2vnunb  30578  fusgreg2wsp  30624  lpni  30769  nmobndseqi  31068  hhcmpl  31489  shne0i  31737  nmcopexi  32316  nmcfnexi  32340  cdj3lem3b  32729  rexcom4f  32752  reuxfrdf  32774  iunin1f  32839  ofpreima  32947  intimafv  32993  fpwrelmapffslem  33014  tosglblem  33231  xrnarchi  33441  isunit2  33496  isdrng4  33555  dvdsrspss  33640  lsmsnorb  33644  lsmsnorb2  33645  1arithufdlem4  33778  constrconj  34076  ordtconnlem1  34255  lmdvg  34284  esumfsup  34401  reprsuc  34943  reprdifc  34955  bnj168  35060  bnj1185  35122  bnj1542  35186  bnj865  35252  bnj916  35262  bnj983  35280  bnj1176  35334  bnj1189  35338  bnj1296  35350  bnj1398  35363  bnj1450  35379  bnj1463  35384  nummin  35423  fineqvnttrclse  35456  axregszf  35461  onvf1odlem1  35482  loop1cycl  35524  cvmliftlem15  35685  cvmlift2lem12  35701  satfvsuclem2  35747  satfvsucsuc  35752  satfdm  35756  satf0  35759  dmopab3rexdif  35792  rexxfr3dALT  36026  dffr5  36141  dfon2lem9  36176  brbigcup  36283  elfuns  36300  brimage  36311  brimg  36322  dfrecs2  36337  imagesset  36340  brub  36341  brsegle  36495  sumeq2si  36599  prodeq2si  36601  cbvprodvw2  36644  filnetlem4  36777  bj-rexcom4bv  37402  bj-rexcom4b  37403  bj-elsngl  37488  bj-axseprep  37594  bj-rest10  37613  bj-restreg  37624  bj-mpomptALT  37644  nlpineqsn  37937  fvineqsneq  37941  iundif1  38128  matunitlindflem1  38150  poimirlem1  38155  poimirlem30  38184  poimirlem32  38186  poimir  38187  ismblfin  38195  volsupnfl  38199  itg2addnclem3  38207  fdc  38279  isfldidl  38602  eldmqsres2  38828  n0elqs  38866  rnxrncnvepres  38957  rnxrnidres  38958  dfcoels  39054  br1cossinres  39071  br1cossinidres  39073  br1cossincnvepres  39074  br1cossxrnidres  39075  br1cossxrncnvepres  39076  br1cossxrncnvssrres  39122  eldmqs1cossres  39278  disjdmqscossss  39440  prtlem10  39524  prter2  39540  islshpat  39676  lshpsmreu  39768  2dim  40129  islpln5  40194  lplnexatN  40222  islvol5  40238  dalem18  40340  dalem20  40352  lhpexle2  40669  lhpexle3  40671  lhpex2leN  40672  4atex2  40736  4atex2-0bOLDN  40738  cdlemftr3  41224  cdlemg17pq  41331  cdlemg19  41343  cdlemg21  41345  cdlemg33d  41368  dva1dim  41644  dih1dimatlem  41988  dihglb2  42001  dvh2dim  42104  mapdrvallem2  42304  mapdpglem3  42334  hdmapglem7a  42586  hashnexinjle  42781  aks6d1c5  42791  supinf  42893  fimgmcyclem  43186  dffltz  43251  elrfirn  43311  isnacs2  43322  isnacs3  43326  sbc2rex  43401  4rexfrabdioph  43410  eldioph4b  43423  fphpd  43428  fiphp3d  43431  rencldnfilem  43432  rmxdioph  43628  expdiophlem1  43633  islnm2  43690  onmaxnelsup  43835  onsupnmax  43840  onsupuni  43841  onsupmaxb  43851  tfsconcatlem  43948  tfsconcatrn  43954  oadif1lem  43991  oadif1  43992  elimaint  44260  cnviun  44261  imaiun1  44262  coiun1  44263  elintima  44264  briunov2  44293  clsk3nimkb  44651  expandrexn  44886  prmunb2  44906  zfregs2VD  45434  n0abso  45570  sswfaxreg  45581  evth2f  45620  evthf  45632  ndisj2  45656  rexanuz2nf  46091  fnlimabslt  46278  climbddf  46286  limsupub  46303  limsuppnflem  46309  limsupubuz  46312  limsupre2lem  46323  limsupreuz  46336  limsupvaluz2  46337  cnrefiisplem  46428  cnrefiisp  46429  stoweidlem28  46627  fourierdlem63  46768  fourierdlem65  46770  fourierdlem89  46794  fourierdlem90  46795  fourierdlem91  46796  fourierdlem100  46805  sge0pnfmpt  47044  ovn0  47165  smfaddlem1  47362  smflimlem4  47373  fsetsniunop  47668  2rexsb  47720  2rexrsb  47721  cbvrex2  47723  2reu8i  47732  clnbgrsym  48485  isubgr3stgrlem6  48618  copisnmnd  48816  pgrpgt2nabl  49024  islindeps  49111  lindslinindsimp1  49115  lindslinindsimp2  49121  islindeps2  49141  islininds2  49142  isldepslvec2  49143  ldepslinc  49167  sepnsepolem1  49578