Theorem rspcev 2929

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcev	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2924	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823

This theorem is used by:  rspcedvdw  2936  rspceaimv  2938  rspc2ev  2945  rspc3ev  2947  rspceeqv  2948  reu6i  3017  rspesbca  3137  brralrspcev  4189  nn0suc  4751  elrnmpt1s  5032  elrnrexdm  5847  eldmrexrn  5849  foco2  5959  elabrex  5963  elabrexg  5964  f1elima  5979  fcofo  5990  fliftfun  6002  fliftval  6006  f1oiso2  6033  fo1st  6391  fo2nd  6392  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllemres  6633  rdgss  6654  frecabcl  6670  nnaordex  6801  nnawordex  6802  ecelqsg  6862  snfig  7103  nnfi  7174  findcard  7192  fimax2gtrilemstep  7205  unsnfi  7226  eqsupti  7337  supmaxti  7345  supisoex  7350  infminti  7368  finomni  7481  nninfwlpoimlemginf  7517  isnumi  7528  oncardval  7532  archnqq  7785  prarloclemarch2  7787  prcdnql  7852  prcunqu  7853  prarloclemlo  7862  prarloclem5  7868  nqprm  7910  1idprl  7958  1idpru  7959  ltexpri  7981  prplnqu  7988  recexprlemm  7992  recexprlem1ssl  8001  recexprlem1ssu  8002  recexpr  8006  aptiprleml  8007  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemloc  8020  cauappcvgprlem1  8027  cauappcvgprlem2  8028  cauappcvgpr  8030  caucvgprlemm  8036  caucvgprlemloc  8043  caucvgprlem1  8047  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgprpr  8080  suplocexprlemmu  8086  suplocexprlemloc  8089  suplocexpr  8093  negexsr  8140  recexgt0sr  8141  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  suplocsrlem  8176  axrnegex  8247  axprecex  8248  nntopi  8262  axcaucvglemres  8267  axpre-suploclemres  8269  cnegex  8506  recexre  8909  recexap  8984  receuap  9002  rerecapb  9176  sup3exmid  9290  cju  9294  nn2ge  9340  nominpos  9548  zdiv  9739  btwnz  9770  supinfneg  10005  infsupneg  10006  ublbneg  10023  lbzbi  10026  zq  10036  z2ge  10239  iccsupr  10379  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  zsupssdc  10684  exbtwnzlemstep  10693  exbtwnzlemex  10695  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnre  10702  qbtwnxr  10703  expnbnd  11116  hashunlem  11260  iswrdinn0  11325  shftlem  11597  shftfvalg  11599  shftfval  11602  caucvgre  11763  cvg1nlemres  11767  rexanuz  11770  rexuz3  11772  resqrexlemex  11807  caubnd2  11900  maxabslemval  11991  maxleast  11996  rexanre  12003  rexico  12004  fimaxre2  12010  minmax  12014  xrmaxiflemval  12035  xrmaxaddlem  12045  xrminmax  12050  climconst  12075  climshftlemg  12087  cn1lem  12099  serf0  12137  zsumdc  12170  fsum3  12173  fsum3cvg3  12182  mertenslemi1  12321  ntrivcvgap0  12335  zproddc  12365  fprodseq  12369  fprodntrivap  12370  dvdsval2  12576  dvds0lem  12587  dvds1lem  12588  dvds2lem  12589  odd2np1lem  12658  odd2np1  12659  opeo  12683  omeo  12684  divalglemex  12708  bezoutlemnewy  12792  bezoutlemaz  12799  bezoutlembz  12800  bezoutlemsup  12805  nnwodc  12832  uzwodc  12833  ncoprmgcdne1b  12886  exprmfct  12936  reumodprminv  13055  modprm0  13056  nnnn0modprm0  13057  pythagtriplem19  13084  pcprmpw2  13135  pockthi  13160  infpnlem2  13162  ballotfilem4  13293  ballotfilemic  13302  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemrn  13362  ennnfonelemnn0  13365  ennnfonelemim  13367  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctinf  13373  ctiunctlemf  13381  ismgmid2  13753  mgmidsssn0  13757  ismndd  13803  isgrpd2  13879  isgrpd  13881  imasgrp2  13966  mhmmnd  13972  ghmgrp  13974  dvdsrmuld  14487  dvdsr01  14495  rhmdvdsr  14566  lspf  14810  lspval  14811  lssats2  14835  aspval  15099  fiinbas  15241  topbas  15259  clsval  15303  neiint  15337  neipsm  15346  opnneissb  15347  opnssneib  15348  innei  15355  restbasg  15360  lmconst  15408  iscnp4  15410  cncnpi  15420  cnconst2  15425  cnptoprest  15431  cnpdis  15434  neitx  15460  txcnp  15463  blssps  15619  blss  15620  blssexps  15621  blssex  15622  ssblex  15623  blin2  15624  neibl  15683  metss2  15690  bdmopn  15696  metrest  15698  metcnp3  15703  tgioo  15746  tgqioo  15747  addcncntoplem  15753  cnopnap  15803  dedekindeulemuub  15809  suplociccreex  15816  dedekindicclemuub  15818  ivthinclemlm  15826  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthreinc  15837  elply2  15927  reeff1oleme  15964  sin0pilem2  15975  sgmnncl  16218  dvdsppwf1o  16244  perfect  16262  bpos1lem  16270  bj-nn0suc0  17142  bj-inf2vnlem1  17162  3dom  17184  nninfsellemeq  17223  nninfomnilem  17227  qdencn  17238  trirec0  17260  qdiff  17265