Theorem rexbii 3170

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

Syntax hints:   ↔ wb 209   ∈ wcel 2110  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-rex 3067

This theorem is referenced by:  2rexbii  3171  2ex2rexrot  3173  rexcom4a  3174  r19.29imd  3178  rexnal2  3179  r19.41vv  3262  r19.42v  3263  r19.43  3264  rexcom  3268  rexcom13  3272  rexrot4  3274  3reeanv  3280  2ralor  3281  cbvrex2vw  3372  cbvrex2v  3375  rexcom4b  3437  ceqsrex2v  3565  clel5  3574  reu7  3645  2reu5a  3657  0el  4275  n0snor2el  4744  uni0b  4847  iuncom  4911  iuncom4  4912  iuniin  4916  dfiunv2  4944  iunab  4960  iunsn  4974  iunn0  4975  iunin2  4979  iundif2  4982  iunun  5001  iunxiun  5005  iunpwss  5015  axrep6  5186  inuni  5236  reusv2lem5  5295  iunopab  5440  dffr2  5515  dffr2ALT  5516  frc  5517  frminex  5531  dfepfr  5536  epfrc  5537  xpiundi  5619  xpiundir  5620  reliin  5687  iunxpf  5717  cnvuni  5755  dmiun  5782  dmopab2rex  5786  elres  5890  elidinxp  5911  dfima3  5932  dffr3  5967  rniun  6011  xpdifid  6031  dminxp  6043  imaco  6115  coiun  6120  dffr4  6178  frpomin2  6195  tz6.26  6201  sucel  6286  isarep1  6468  rexrn  6906  ralrn  6907  elrnrexdmb  6909  fnasrn  6960  rexima  7053  ralima  7054  abrexco  7057  imaiun  7058  fliftcnv  7120  rexrnmpo  7349  iunpw  7556  abrexex2g  7737  el2xptp  7807  frrlem9  8035  rdglem1  8151  tz7.49  8181  oarec  8290  omeu  8313  qsid  8465  eroveu  8494  ixp0  8612  fimax2g  8917  marypha2lem2  9052  dfsup2  9060  infcllem  9103  dfoi  9127  wemapsolem  9166  zfregcl  9210  zfreg  9211  zfregfr  9220  oemapso  9297  zfregs2  9349  infenaleph  9705  isinfcard  9706  kmlem7  9770  kmlem13  9776  fin23lem26  9939  dffin1-5  10002  fin12  10027  numth  10086  ac6n  10099  zorn2lem7  10116  zorng  10118  brdom7disj  10145  brdom6disj  10146  uniwun  10354  axgroth5  10438  axgroth4  10446  grothprim  10448  npomex  10610  genpass  10623  elreal  10745  dfinfre  11813  infrenegsup  11815  uzwo  12507  ublbneg  12529  xrinfmss2  12901  4fvwrd4  13232  fsuppmapnn0fiubex  13565  fsuppmapnn0ub  13568  mptnn0fsuppr  13572  hashge2el2dif  14046  dfrtrclrec2  14621  rexanuz  14909  rexfiuz  14911  clim0  15067  cbvsum  15259  incexc2  15402  cbvprod  15477  fprodle  15558  iprodmul  15565  divalglem10  15963  divalgb  15965  ncoprmlnprm  16284  pythagtriplem2  16370  pythagtriplem19  16386  pythagtrip  16387  pceu  16399  prmreclem6  16474  4sqlem12  16509  cshwshashlem1  16649  cshwshash  16658  imasaddfnlem  17033  isdrs2  17813  smndex1mgm  18334  smndex1n0mnd  18339  pmtrprfvalrn  18880  pgpfac1lem5  19466  dvdsrval  19663  opprunit  19679  lsmspsn  20121  lsmelval2  20122  islpidl  20284  mat1dimelbas  21368  mat1dimbas  21369  mdetunilem8  21516  pmatcollpw2lem  21674  tgval2  21853  ntreq0  21974  isclo2  21985  neiptopnei  22029  ist0-3  22242  tgcmp  22298  cmpfi  22305  is1stc2  22339  unisngl  22424  xkobval  22483  txtube  22537  txcmplem1  22538  xkococnlem  22556  eltsms  23030  metrest  23422  iscau3  24175  bcth  24226  pmltpc  24347  itg2i1fseq  24653  itg2cn  24661  plyun0  25091  aaliou3lem9  25243  1cubr  25725  dchrvmasumlema  26381  selbergsb  26456  ostth  26520  istrkg2ld  26551  tglowdim1i  26592  legtrid  26682  midex  26828  ishpg  26850  brbtwn2  26996  colinearalg  27001  ax5seg  27029  axpasch  27032  axlowdimlem6  27038  axeuclidlem  27053  axeuclid  27054  elntg2  27076  umgr2edg1  27299  umgr2edgneu  27302  nbgrsym  27451  isuvtx  27483  usgr2pth0  27852  wlkiswwlksupgr2  27961  clwwlknun  28195  4cycl2vnunb  28373  fusgreg2wsp  28419  lpni  28561  nmobndseqi  28860  hhcmpl  29281  shne0i  29529  nmcopexi  30108  nmcfnexi  30132  cdj3lem3b  30521  rexcom4f  30538  reuxfrdf  30558  iunin1f  30616  ofpreima  30722  intimafv  30763  fpwrelmapffslem  30787  tosglblem  30971  xrnarchi  31157  lsmsnorb  31293  lsmsnorb2  31294  ordtconnlem1  31588  lmdvg  31617  esumfsup  31750  reprsuc  32307  reprdifc  32319  bnj168  32421  bnj1185  32486  bnj1542  32550  bnj865  32616  bnj916  32626  bnj983  32644  bnj1176  32698  bnj1189  32702  bnj1296  32714  bnj1398  32727  bnj1450  32743  bnj1463  32748  nummin  32776  loop1cycl  32812  cvmliftlem15  32973  cvmlift2lem12  32989  satfvsuclem2  33035  satfvsucsuc  33040  satfdm  33044  satf0  33047  dmopab3rexdif  33080  imaeqsexv  33406  dffr5  33439  imaindm  33472  dfon2lem9  33486  brttrcl2  33513  ttrclresv  33516  poxp2  33527  poxp3  33533  soseq  33540  noseponlem  33604  nosepon  33605  nolt02o  33635  noinfbnd1lem1  33663  noinfbnd1lem4  33666  elold  33790  made0  33794  lrrecfr  33837  brbigcup  33937  elfuns  33954  brimage  33965  brimg  33976  dfrecs2  33989  imagesset  33992  brub  33993  brsegle  34147  filnetlem4  34307  bj-rexcom4bv  34804  bj-rexcom4b  34805  bj-elsngl  34895  bj-rest10  34994  bj-restreg  35005  bj-mpomptALT  35025  nlpineqsn  35316  fvineqsneq  35320  iundif1  35488  matunitlindflem1  35510  poimirlem1  35515  poimirlem30  35544  poimirlem32  35546  poimir  35547  ismblfin  35555  volsupnfl  35559  itg2addnclem3  35567  fdc  35640  isfldidl  35963  eldmqsres2  36159  n0elqs  36198  rnxrncnvepres  36263  rnxrnidres  36264  dfcoels  36290  br1cossinres  36302  br1cossinidres  36304  br1cossincnvepres  36305  br1cossxrnidres  36306  br1cossxrncnvepres  36307  br1cossxrncnvssrres  36363  eldmqs1cossres  36508  prtlem10  36616  prter2  36632  islshpat  36768  lshpsmreu  36860  2dim  37221  islpln5  37286  lplnexatN  37314  islvol5  37330  dalem18  37432  dalem20  37444  lhpexle2  37761  lhpexle3  37763  lhpex2leN  37764  4atex2  37828  4atex2-0bOLDN  37830  cdlemftr3  38316  cdlemg17pq  38423  cdlemg19  38435  cdlemg21  38437  cdlemg33d  38460  dva1dim  38736  dih1dimatlem  39080  dihglb2  39093  dvh2dim  39196  mapdrvallem2  39396  mapdpglem3  39426  hdmapglem7a  39678  dffltz  40174  elrfirn  40220  isnacs2  40231  isnacs3  40235  sbc2rex  40312  4rexfrabdioph  40323  eldioph4b  40336  fphpd  40341  fiphp3d  40344  rencldnfilem  40345  rmxdioph  40541  expdiophlem1  40546  islnm2  40606  elimaint  40933  cnviun  40935  imaiun1  40936  coiun1  40937  elintima  40938  briunov2  40967  clsk3nimkb  41327  expandrexn  41582  prmunb2  41602  zfregs2VD  42134  evth2f  42231  evthf  42243  ndisj2  42272  fnlimabslt  42895  climbddf  42903  limsupub  42920  limsuppnflem  42926  limsupubuz  42929  limsupre2lem  42940  limsupreuz  42953  limsupvaluz2  42954  cnrefiisplem  43045  cnrefiisp  43046  stoweidlem28  43244  fourierdlem63  43385  fourierdlem65  43387  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem100  43422  sge0pnfmpt  43658  ovn0  43779  smfaddlem1  43970  smflimlem4  43981  fsetsniunop  44215  2rexsb  44265  2rexrsb  44266  cbvrex2  44268  2reu8i  44277  copisnmnd  45036  pgrpgt2nabl  45375  islindeps  45467  lindslinindsimp1  45471  lindslinindsimp2  45477  islindeps2  45497  islininds2  45498  isldepslvec2  45499  ldepslinc  45523  sepnsepolem1  45888