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  4190  nn0suc  4753  elrnmpt1s  5034  elrnrexdm  5850  eldmrexrn  5852  foco2  5962  elabrex  5966  elabrexg  5967  f1elima  5982  fcofo  5993  fliftfun  6005  fliftval  6009  f1oiso2  6036  fo1st  6395  fo2nd  6396  tfr0dm  6597  tfrlemisucaccv  6600  tfrlemi14d  6608  tfrexlem  6609  tfr1onlemsucaccv  6616  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllemres  6637  rdgss  6658  frecabcl  6674  nnaordex  6805  nnawordex  6806  ecelqsg  6866  snfig  7107  nnfi  7178  findcard  7196  fimax2gtrilemstep  7209  unsnfi  7230  eqsupti  7342  supmaxti  7350  supisoex  7355  infminti  7373  finomni  7486  nninfwlpoimlemginf  7522  isnumi  7533  oncardval  7537  archnqq  7790  prarloclemarch2  7792  prcdnql  7857  prcunqu  7858  prarloclemlo  7867  prarloclem5  7873  nqprm  7915  1idprl  7963  1idpru  7964  ltexpri  7986  prplnqu  7993  recexprlemm  7997  recexprlem1ssl  8006  recexprlem1ssu  8007  recexpr  8011  aptiprleml  8012  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemloc  8025  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgpr  8035  caucvgprlemm  8041  caucvgprlemloc  8048  caucvgprlem1  8052  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgprpr  8085  suplocexprlemmu  8091  suplocexprlemloc  8094  suplocexpr  8098  negexsr  8145  recexgt0sr  8146  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  suplocsrlem  8181  axrnegex  8252  axprecex  8253  nntopi  8267  axcaucvglemres  8272  axpre-suploclemres  8274  cnegex  8511  recexre  8914  recexap  8989  receuap  9007  rerecapb  9181  sup3exmid  9295  cju  9299  nn2ge  9346  nominpos  9554  zdiv  9745  btwnz  9776  supinfneg  10011  infsupneg  10012  ublbneg  10029  lbzbi  10032  zq  10042  z2ge  10245  iccsupr  10385  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  zsupssdc  10690  exbtwnzlemstep  10699  exbtwnzlemex  10701  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnre  10708  qbtwnxr  10709  expnbnd  11122  hashunlem  11266  iswrdinn0  11331  shftlem  11603  shftfvalg  11605  shftfval  11608  caucvgre  11769  cvg1nlemres  11773  rexanuz  11776  rexuz3  11778  resqrexlemex  11813  caubnd2  11906  maxabslemval  11997  maxleast  12002  rexanre  12009  rexico  12010  fimaxre2  12016  minmax  12020  xrmaxiflemval  12041  xrmaxaddlem  12051  xrminmax  12056  climconst  12081  climshftlemg  12093  cn1lem  12105  serf0  12143  zsumdc  12176  fsum3  12179  fsum3cvg3  12188  mertenslemi1  12327  ntrivcvgap0  12341  zproddc  12371  fprodseq  12375  fprodntrivap  12376  dvdsval2  12582  dvds0lem  12593  dvds1lem  12594  dvds2lem  12595  odd2np1lem  12664  odd2np1  12665  opeo  12689  omeo  12690  divalglemex  12714  bezoutlemnewy  12798  bezoutlemaz  12805  bezoutlembz  12806  bezoutlemsup  12811  nnwodc  12838  uzwodc  12839  ncoprmgcdne1b  12892  exprmfct  12942  reumodprminv  13061  modprm0  13062  nnnn0modprm0  13063  pythagtriplem19  13090  pcprmpw2  13141  pockthi  13166  infpnlem2  13168  ballotfilem4  13299  ballotfilemic  13308  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemrn  13368  ennnfonelemnn0  13371  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  ctiunctlemf  13387  ismgmid2  13759  mgmidsssn0  13763  ismndd  13809  isgrpd2  13885  isgrpd  13887  imasgrp2  13972  mhmmnd  13978  ghmgrp  13980  dvdsrmuld  14512  dvdsr01  14520  rhmdvdsr  14591  lspf  14835  lspval  14836  lssats2  14860  aspval  15124  fiinbas  15275  topbas  15293  clsval  15337  neiint  15371  neipsm  15380  opnneissb  15381  opnssneib  15382  innei  15389  restbasg  15394  lmconst  15442  iscnp4  15444  cncnpi  15454  cnconst2  15459  cnptoprest  15465  cnpdis  15468  neitx  15494  txcnp  15497  blssps  15653  blss  15654  blssexps  15655  blssex  15656  ssblex  15657  blin2  15658  neibl  15717  metss2  15724  bdmopn  15730  metrest  15732  metcnp3  15737  tgioo  15780  tgqioo  15781  addcncntoplem  15787  cnopnap  15837  dedekindeulemuub  15843  suplociccreex  15850  dedekindicclemuub  15852  ivthinclemlm  15860  ivthinclemum  15861  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthreinc  15871  elply2  15961  reeff1oleme  15998  sin0pilem2  16009  sgmnncl  16257  dvdsppwf1o  16283  perfect  16301  bpos1lem  16309  bj-nn0suc0  17181  bj-inf2vnlem1  17201  3dom  17223  nninfsellemeq  17263  nninfomnilem  17267  qdencn  17278  trirec0  17300  qdiff  17305