Theorem rexbii 3177

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  2rexbii  3178  2ex2rexrot  3180  rexcom4a  3181  r19.29imd  3185  rexnal2  3186  r19.41vv  3275  r19.42v  3276  r19.43  3277  rexcom  3281  rexcom13  3285  rexrot4  3287  3reeanv  3293  2ralorOLD  3295  cbvrex2vw  3386  cbvrex2v  3389  rexcom4b  3451  ceqsrex2v  3580  clel5  3589  reu7  3662  2reu5a  3674  0el  4291  n0snor2el  4761  uni0b  4864  iuncom  4928  iuncom4  4929  iuniin  4933  dfiunv2  4961  iunab  4977  iunsn  4991  iunn0  4992  iunin2  4996  iundif2  4999  iunun  5018  iunxiun  5022  iunpwss  5032  axrep6  5212  inuni  5262  reusv2lem5  5320  iunopab  5465  dffr2  5544  dffr2ALT  5545  frc  5546  frminex  5560  dfepfr  5565  epfrc  5566  xpiundi  5648  xpiundir  5649  reliin  5716  iunxpf  5746  cnvuni  5784  dmiun  5811  dmopab2rex  5815  elres  5919  elidinxp  5940  dfima3  5961  dffr3  5996  rniun  6040  xpdifid  6060  dminxp  6072  imaco  6144  coiun  6149  dffr4  6211  frpomin2  6229  tz6.26OLD  6236  sucel  6324  isarep1  6506  rexrn  6945  ralrn  6946  elrnrexdmb  6948  fnasrn  6999  rexima  7095  ralima  7096  abrexco  7099  imaiun  7100  fliftcnv  7162  rexrnmpo  7391  iunpw  7599  abrexex2g  7780  el2xptp  7850  frrlem9  8081  rdglem1  8217  tz7.49  8246  oarec  8355  omeu  8378  qsid  8530  eroveu  8559  ixp0  8677  fimax2g  8990  marypha2lem2  9125  dfsup2  9133  infcllem  9176  dfoi  9200  wemapsolem  9239  zfregcl  9283  zfreg  9284  zfregfr  9293  oemapso  9370  zfregs2  9422  infenaleph  9778  isinfcard  9779  kmlem7  9843  kmlem13  9849  fin23lem26  10012  dffin1-5  10075  fin12  10100  numth  10159  ac6n  10172  zorn2lem7  10189  zorng  10191  brdom7disj  10218  brdom6disj  10219  uniwun  10427  axgroth5  10511  axgroth4  10519  grothprim  10521  npomex  10683  genpass  10696  elreal  10818  dfinfre  11886  infrenegsup  11888  uzwo  12580  ublbneg  12602  xrinfmss2  12974  4fvwrd4  13305  fsuppmapnn0fiubex  13640  fsuppmapnn0ub  13643  mptnn0fsuppr  13647  hashge2el2dif  14122  dfrtrclrec2  14697  rexanuz  14985  rexfiuz  14987  clim0  15143  cbvsum  15335  incexc2  15478  cbvprod  15553  fprodle  15634  iprodmul  15641  divalglem10  16039  divalgb  16041  ncoprmlnprm  16360  pythagtriplem2  16446  pythagtriplem19  16462  pythagtrip  16463  pceu  16475  prmreclem6  16550  4sqlem12  16585  cshwshashlem1  16725  cshwshash  16734  imasaddfnlem  17156  isdrs2  17939  smndex1mgm  18461  smndex1n0mnd  18466  pmtrprfvalrn  19011  pgpfac1lem5  19597  dvdsrval  19802  opprunit  19818  lsmspsn  20261  lsmelval2  20262  islpidl  20430  mat1dimelbas  21528  mat1dimbas  21529  mdetunilem8  21676  pmatcollpw2lem  21834  tgval2  22014  ntreq0  22136  isclo2  22147  neiptopnei  22191  ist0-3  22404  tgcmp  22460  cmpfi  22467  is1stc2  22501  unisngl  22586  xkobval  22645  txtube  22699  txcmplem1  22700  xkococnlem  22718  eltsms  23192  metrest  23586  iscau3  24347  bcth  24398  pmltpc  24519  itg2i1fseq  24825  itg2cn  24833  plyun0  25263  aaliou3lem9  25415  1cubr  25897  dchrvmasumlema  26553  selbergsb  26628  ostth  26692  istrkg2ld  26725  tglowdim1i  26766  legtrid  26856  midex  27002  ishpg  27024  brbtwn2  27176  colinearalg  27181  ax5seg  27209  axpasch  27212  axlowdimlem6  27218  axeuclidlem  27233  axeuclid  27234  elntg2  27256  umgr2edg1  27481  umgr2edgneu  27484  nbgrsym  27633  isuvtx  27665  usgr2pth0  28034  wlkiswwlksupgr2  28143  clwwlknun  28377  4cycl2vnunb  28555  fusgreg2wsp  28601  lpni  28743  nmobndseqi  29042  hhcmpl  29463  shne0i  29711  nmcopexi  30290  nmcfnexi  30314  cdj3lem3b  30703  rexcom4f  30720  reuxfrdf  30740  iunin1f  30798  ofpreima  30904  intimafv  30945  fpwrelmapffslem  30969  tosglblem  31154  xrnarchi  31340  lsmsnorb  31481  lsmsnorb2  31482  ordtconnlem1  31776  lmdvg  31805  esumfsup  31938  reprsuc  32495  reprdifc  32507  bnj168  32609  bnj1185  32673  bnj1542  32737  bnj865  32803  bnj916  32813  bnj983  32831  bnj1176  32885  bnj1189  32889  bnj1296  32901  bnj1398  32914  bnj1450  32930  bnj1463  32935  nummin  32963  loop1cycl  32999  cvmliftlem15  33160  cvmlift2lem12  33176  satfvsuclem2  33222  satfvsucsuc  33227  satfdm  33231  satf0  33234  dmopab3rexdif  33267  imaeqsexv  33593  dffr5  33627  imaindm  33659  dfon2lem9  33673  brttrcl2  33700  ttrclresv  33703  poxp2  33717  poxp3  33723  soseq  33730  noseponlem  33794  nosepon  33795  nolt02o  33825  noinfbnd1lem1  33853  noinfbnd1lem4  33856  elold  33980  made0  33984  lrrecfr  34027  brbigcup  34127  elfuns  34144  brimage  34155  brimg  34166  dfrecs2  34179  imagesset  34182  brub  34183  brsegle  34337  filnetlem4  34497  bj-rexcom4bv  34994  bj-rexcom4b  34995  bj-elsngl  35085  bj-rest10  35186  bj-restreg  35197  bj-mpomptALT  35217  nlpineqsn  35506  fvineqsneq  35510  iundif1  35678  matunitlindflem1  35700  poimirlem1  35705  poimirlem30  35734  poimirlem32  35736  poimir  35737  ismblfin  35745  volsupnfl  35749  itg2addnclem3  35757  fdc  35830  isfldidl  36153  eldmqsres2  36349  n0elqs  36388  rnxrncnvepres  36453  rnxrnidres  36454  dfcoels  36480  br1cossinres  36492  br1cossinidres  36494  br1cossincnvepres  36495  br1cossxrnidres  36496  br1cossxrncnvepres  36497  br1cossxrncnvssrres  36553  eldmqs1cossres  36698  prtlem10  36806  prter2  36822  islshpat  36958  lshpsmreu  37050  2dim  37411  islpln5  37476  lplnexatN  37504  islvol5  37520  dalem18  37622  dalem20  37634  lhpexle2  37951  lhpexle3  37953  lhpex2leN  37954  4atex2  38018  4atex2-0bOLDN  38020  cdlemftr3  38506  cdlemg17pq  38613  cdlemg19  38625  cdlemg21  38627  cdlemg33d  38650  dva1dim  38926  dih1dimatlem  39270  dihglb2  39283  dvh2dim  39386  mapdrvallem2  39586  mapdpglem3  39616  hdmapglem7a  39868  dffltz  40387  elrfirn  40433  isnacs2  40444  isnacs3  40448  sbc2rex  40525  4rexfrabdioph  40536  eldioph4b  40549  fphpd  40554  fiphp3d  40557  rencldnfilem  40558  rmxdioph  40754  expdiophlem1  40759  islnm2  40819  elimaint  41146  cnviun  41147  imaiun1  41148  coiun1  41149  elintima  41150  briunov2  41179  clsk3nimkb  41539  expandrexn  41798  prmunb2  41818  zfregs2VD  42350  evth2f  42447  evthf  42459  ndisj2  42488  fnlimabslt  43110  climbddf  43118  limsupub  43135  limsuppnflem  43141  limsupubuz  43144  limsupre2lem  43155  limsupreuz  43168  limsupvaluz2  43169  cnrefiisplem  43260  cnrefiisp  43261  stoweidlem28  43459  fourierdlem63  43600  fourierdlem65  43602  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem100  43637  sge0pnfmpt  43873  ovn0  43994  smfaddlem1  44185  smflimlem4  44196  fsetsniunop  44430  2rexsb  44480  2rexrsb  44481  cbvrex2  44483  2reu8i  44492  copisnmnd  45251  pgrpgt2nabl  45590  islindeps  45682  lindslinindsimp1  45686  lindslinindsimp2  45692  islindeps2  45712  islininds2  45713  isldepslvec2  45714  ldepslinc  45738  sepnsepolem1  46103