Theorem rspcev 3554

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 1890	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 3549	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1520   ∈ wcel 2079  ∃wrex 3104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rex 3109  df-v 3434

This theorem is referenced by:  rspceaimv  3562  rspc2ev  3569  rspc3ev  3571  rspceeqv  3572  reu6i  3648  rspesbca  3787  eliuni  4825  brralrspcev  5016  wefrc  5429  wereu2  5432  xpdifid  5893  onfr  6097  ordunidif  6106  eliman0  6565  dffv2  6615  elrnrexdm  6711  eldmrexrn  6713  elabrex  6858  f1elima  6877  fliftfun  6919  fliftval  6923  f1oiso2  6959  sorpssuni  7307  sorpssint  7308  onssmin  7359  onminex  7369  tfrlem12  7868  seqomlem2  7929  oawordeulem  8021  oaass  8028  odi  8046  omass  8047  omeulem1  8049  oen0  8053  oelim2  8062  oeeulem  8068  nnawordex  8104  boxcutc  8343  snfi  8432  onfin  8545  pssnn  8572  ssnnfi  8573  dif1en  8587  findcard  8593  frfi  8599  fisupg  8602  nnsdomg  8613  unfi  8621  fissuni  8665  fipreima  8666  finsschain  8667  indexfi  8668  marypha1lem  8733  eqsup  8756  supmax  8767  fisup2g  8768  fisupcl  8769  supisoex  8774  infmin  8794  fiinfg  8799  fiinf2g  8800  wofib  8845  wemaplem2  8847  card2inf  8855  brwdom2  8873  cnfcom3clem  9003  trcl  9005  r1ordg  9042  r1pwss  9048  tz9.12lem3  9053  tz9.12  9054  r1elwf  9060  tcrank  9148  scottex  9149  scott0  9150  isnumi  9210  onsdom  9260  ondomen  9298  infpwfien  9323  cardaleph  9350  infenaleph  9352  alephfplem4  9368  alephfp2  9370  dfac2b  9391  ackbij1lem18  9494  ackbij1  9495  cflem  9503  cflecard  9510  cfsuc  9514  cfflb  9516  cofsmo  9526  coftr  9530  fin23lem7  9573  fin23lem11  9574  enfin2i  9578  fin23lem26  9582  isf32lem5  9614  isf34lem4  9634  isfin1-3  9643  fin1a2lem7  9663  axdc3lem4  9710  ttukeylem7  9772  iunfo  9796  ficard  9822  pwcfsdom  9840  fpwwe2lem12  9898  wunex  9996  eltsk2g  10008  grur1  10077  axgroth6  10085  inaprc  10093  nqereu  10186  archnq  10237  genpnmax  10264  ltexpri  10300  prlem936  10304  recexpr  10308  supexpr  10311  negexsr  10359  recexsrlem  10360  recexsr  10364  supsrlem  10368  axrnegex  10419  axrrecex  10420  axpre-sup  10426  1re  10476  dedekind  10639  dedekindle  10640  cnegex  10657  cnegex2  10658  recex  11109  receu  11122  cju  11471  nn2ge  11501  nominpos  11711  zdiv  11890  btwnz  11922  uzwo  12149  ublbneg  12171  lbzbi  12174  zsupss  12175  uzsupss  12178  rpnnen1lem1  12216  rpnnen1lem3  12217  rpnnen1lem4  12218  rpnnen1lem5  12219  z2ge  12430  qbtwnre  12431  qbtwnxr  12432  xralrple  12437  xrsupsslem  12539  xrinfmsslem  12540  supxrpnf  12550  icc0  12625  uzsup  13069  expnbnd  13431  expmulnbnd  13434  hashkf  13530  hashdom  13576  iswrdi  13699  rtrclreclem1  14239  rtrclreclem2  14240  rtrclreclem3  14241  01sqrex  14431  resqrex  14432  sqrtneg  14449  abs1m  14517  rexanuz  14527  rexuz3  14530  rexuzre  14534  sqreu  14542  o1lo1  14716  climconst  14722  rlimclim1  14724  climshftlem  14753  rlimo1  14795  lo1add  14805  lo1mul  14806  lo1le  14830  isercoll  14846  serf0  14859  zsum  14896  fsum  14898  fsumcvg3  14907  mertenslem1  15061  ntrivcvgn0  15075  ntrivcvgmullem  15078  zprod  15112  fprod  15116  fprodntriv  15117  dvdsval2  15431  dvds0lem  15441  dvds1lem  15442  dvds2lem  15443  odd2np1lem  15510  odd2np1  15511  opeo  15535  omeo  15536  divalglem9  15573  gcdcllem3  15671  lcmcllem  15757  qredeu  15819  exprmfct  15865  isprm5  15868  odzcllem  15946  reumodprminv  15958  modprm0  15959  nnnn0modprm0  15960  pythagtriplem19  15987  pcprmpw2  16035  pockthi  16060  infpnlem2  16064  vdwlem2  16135  vdwlem10  16143  vdwlem13  16146  ramub1lem1  16179  cshwrepswhash1  16253  imasleval  16631  mreexexlem3d  16734  mreexexlem4d  16735  iscatd  16761  poslubd  17575  fpwipodrs  17591  ismgmid2  17694  mgmidsssn0  17696  gsumval2a  17706  ismndd  17740  isgrpd2  17869  isgrpd  17871  imasgrp2  17959  mhmmnd  17966  ghmgrp  17968  gaorber  18167  orbsta  18172  cayleyth  18262  pmtrdifel  18327  pmtrdifwrdel  18332  pmtrdifwrdel2  18333  psgnunilem2  18342  psgnunilem3  18343  psgnvalii  18356  pgpfi1  18438  sylow1lem3  18443  sylow1lem5  18445  pgpfi  18448  sylow2alem2  18461  efgredeu  18593  lt6abl  18724  pgpfac1lem3a  18903  pgpfac1lem3  18904  pgpfac1lem5  18906  pgpfaclem1  18908  pgpfaclem3  18910  ablfaclem2  18913  dvdsrmul  19076  dvdsr01  19083  irredrmul  19135  lspf  19424  lspval  19425  lssats2  19450  lspfixed  19578  lspsolvlem  19592  aspval  19778  evlseu  19971  zringlpir  20306  zncyg  20365  cygth  20388  frlmup4  20615  fiinbas  21232  topbas  21252  pptbas  21288  clsval  21317  elcls  21353  neiint  21384  neips  21393  opnneissb  21394  opnssneib  21395  innei  21405  neiptopnei  21412  restbas  21438  neitr  21460  pnfnei  21500  mnfnei  21501  lmconst  21541  iscnp4  21543  cncnpi  21558  cnconst2  21563  cnprest  21569  cnpdis  21573  nrmsep  21637  regsep2  21656  cmpcovf  21671  cmpsub  21680  cmpcld  21682  hauscmplem  21686  conncompid  21711  2ndci  21728  2ndcsb  21729  2ndc1stc  21731  1stcrest  21733  2ndcctbss  21735  2ndcdisj  21736  2ndcomap  21738  2ndcsep  21739  dis2ndc  21740  restlly  21763  islly2  21764  hausllycmp  21774  cldllycmp  21775  lly1stc  21776  dislly  21777  ssref  21792  refref  21793  finlocfin  21800  dissnlocfin  21809  locfindis  21810  llycmpkgen2  21830  cmpkgen  21831  1stckgenlem  21833  elptr  21853  ptbasfi  21861  neitx  21887  ptpjopn  21892  txcnp  21900  ptcnplem  21901  txlly  21916  txnlly  21917  txtube  21920  txcmplem1  21921  tx1stc  21930  txkgen  21932  xkococnlem  21939  txconn  21969  tgqtop  21992  kqreglem1  22021  kqreglem2  22022  kqnrmlem1  22023  kqnrmlem2  22024  reghmph  22073  nrmhmph  22074  fbssfi  22117  opnfbas  22122  isfil2  22136  fsubbas  22147  ssfg  22152  fgss2  22154  fbasrn  22164  filuni  22165  fgtr  22170  ssufl  22198  uffix  22201  elfm2  22228  elfm3  22230  imaelfm  22231  rnelfmlem  22232  rnelfm  22233  fmfnfmlem4  22237  fmfnfm  22238  fmco  22241  ufldom  22242  hausflim  22261  flimcls  22265  hauspwpwf1  22267  flffbas  22275  txflf  22286  fclscf  22305  fclsfnflim  22307  alexsubALTlem4  22330  alexsubALT  22331  tmdgsum2  22376  symgtgp  22381  subgntr  22386  opnsubg  22387  ghmcnp  22394  qustgpopn  22399  tsmsfbas  22407  tsmsxplem1  22432  ustexsym  22495  elrnust  22504  trust  22509  utoptop  22514  restutop  22517  restutopopn  22518  ustuqtop4  22524  utopsnneiplem  22527  iducn  22563  fmucnd  22572  cfilufg  22573  trcfilu  22574  neipcfilu  22576  imasdsf1olem  22654  blssps  22705  blss  22706  blssexps  22707  blssex  22708  ssblex  22709  blin2  22710  neibl  22782  blcld  22786  metss2  22793  stdbdmopn  22799  met1stc  22802  met2ndci  22803  metrest  22805  prdsxmslem2  22810  metcnp3  22821  metuval  22830  metustexhalf  22837  metustfbas  22838  cfilucfil  22840  restmetu  22851  dscopn  22854  ngptgp  22916  nlmvscnlem1  22966  tgioo  23075  tgqioo  23079  xrsmopn  23091  zcld  23092  recld2  23093  zdis  23095  icccmplem1  23101  icccmplem2  23102  xmetdcn2  23116  addcnlem  23143  xrhmeo  23221  cnheibor  23230  cnllycmp  23231  lebnumlem3  23238  lebnum  23239  xlebnum  23240  lebnumii  23241  elpi1i  23321  ipcnlem1  23519  lmnn  23537  iscfil3  23547  cfilres  23570  flimcfil  23588  bcthlem4  23601  bcthlem5  23602  minveclem4c  23699  minveclem2  23700  minveclem3b  23702  minveclem3  23703  minveclem4  23706  minveclem6  23708  ivthlem2  23724  ivth  23726  ivthle  23728  ivthle2  23729  elovolmr  23748  ovolunlem1  23769  ovoliunlem2  23775  ovolicc1  23788  iundisj  23820  iunmbl2  23829  dyadmbllem  23871  volivth  23879  mbflimsup  23938  i1faddlem  23965  i1fmullem  23966  itg2lr  24002  itg2monolem1  24022  limcnlp  24147  ellimc3  24148  limcflf  24150  limciun  24163  rollelem  24257  c1lip1  24265  lhop1lem  24281  ply1divex  24401  ig1peu  24436  elply2  24457  coeeq  24488  plydivlem3  24555  plydivlem4  24556  elqaalem3  24581  qaa  24583  iaa  24585  aareccl  24586  aannenlem2  24589  aalioulem2  24593  aalioulem3  24594  aalioulem5  24596  aalioulem6  24597  aaliou  24598  aaliou2  24600  aaliou3lem8  24605  ulmshftlem  24648  reeff1o  24706  pilem2  24711  pilem3  24712  efif1olem2  24796  efopn  24910  cxpcn3lem  24997  cxpeq  25007  dcubic2  25091  quart  25108  xrlimcnp  25216  ftalem5  25324  ftalem7  25326  sgmnncl  25394  dvdsppwf1o  25433  musum  25438  perfect  25477  dchrptlem1  25510  dchrptlem2  25511  dchrpt  25513  bpos1lem  25528  lgsqrlem4  25595  lgsdchrval  25600  2sqblem  25677  dchrisumlem3  25737  chpdifbndlem2  25800  pntrsumbnd2  25813  pntpbnd1  25832  pntpbnd2  25833  pntpbnd  25834  pntibndlem2  25837  pntibndlem3  25838  pntleme  25854  pntlem3  25855  axtgcont  25925  tgcgrxfr  25974  legid  26043  btwnleg  26044  leg0  26048  tghilberti1  26093  tglnpt2  26097  colline  26105  mirreu3  26110  isperp2  26171  colperpex  26189  lnopp2hpgb  26219  hpgerlem  26221  brbtwn  26356  brcgr  26357  brbtwn2  26362  axpasch  26398  axlowdimlem14  26412  axlowdim2  26417  axcontlem2  26422  axcontlem4  26424  axcontlem8  26428  axcontlem10  26430  axcontlem12  26432  fusgrn0degnn0  26952  friendshipgt3  27857  lpni  27936  isgrpoi  27954  vacn  28150  smcnlem  28153  nmosetn0  28221  nmoolb  28227  nmobndi  28231  nmoo0  28247  nmlno0lem  28249  isblo3i  28257  blo3i  28258  blocnilem  28260  ubthlem1  28326  minvecolem2  28331  minvecolem3  28332  minvecolem4c  28335  minvecolem4  28336  minvecolem5  28337  minvecolem6  28338  norm1exi  28706  occl  28760  spanval  28789  spancl  28792  shsval2i  28843  ococin  28864  pjoml6i  29045  nmopsetn0  29321  nmfnsetn0  29334  nmoplb  29363  nmfnlb  29380  nmop0  29442  nmfn0  29443  nmlnop0iALT  29451  nmopun  29470  nmcexi  29482  lnconi  29489  lnopcnbd  29492  lnfncnbd  29513  riesz3i  29518  riesz1  29521  cnlnadjlem2  29524  cnlnadjlem8  29530  cnlnadjlem9  29531  adjbd1o  29541  branmfn  29561  opsqrlem1  29596  pjnmopi  29604  strlem1  29706  stri  29713  hstri  29721  cvcon3  29740  cvnbtwn  29742  superpos  29810  shatomici  29814  atcvat4i  29853  mdsymlem2  29860  cdj1i  29889  cdj3i  29897  rexunirn  29935  foresf1o  29942  iundisjf  30005  elunirn2  30059  aciunf1lem  30070  fnpreimac  30079  fgreu  30080  fcnvgreu  30081  xrge0infss  30145  ssnnssfz  30170  iundisjfi  30177  xreceu  30253  rexdiv  30257  isarchi3  30412  archirngz  30414  archiabllem2a  30419  rhmdvdsr  30500  0nellinds  30538  fimaproj  30670  qtophaus  30673  reff  30676  locfinreflem  30677  cmpcref  30687  dispcmp  30696  metidval  30703  pstmval  30708  tpr2rico  30728  pnfneige0  30767  qqhucn  30806  rrhre  30835  indf1ofs  30858  esumcst  30895  esumpcvgval  30910  dmsigagen  30976  rossros  31012  dya2icoseg  31108  dya2iocnrect  31112  dya2iocuni  31114  eulerpartlemgvv  31207  dstfrvunirn  31305  ballotlem4  31329  ballotlemic  31337  ballotlem1c  31338  ballotlemrc  31361  signsw0g  31399  signswmnd  31400  prodfzo03  31447  tgoldbachgt  31507  loop1cycl  31948  umgr2cycllem  31951  umgr2cycl  31952  subfacp1lem3  31993  erdsze2lem2  32015  cnpconn  32041  txpconn  32043  ptpconn  32044  indispconn  32045  connpconn  32046  cvxpconn  32053  cnllysconn  32056  cvmsss2  32085  cvmcov2  32086  cvmopnlem  32089  cvmliftlem14  32108  cvmliftlem15  32109  cvmlift2lem11  32124  cvmlift2lem12  32125  cvmlift2lem13  32126  cvmlift3lem2  32131  cvmlift3lem6  32135  cvmlift3lem9  32138  mthmi  32377  br8  32545  br6  32546  br4  32547  dfon2lem9  32589  trpredtr  32623  dftrpred3g  32626  frpomin  32632  frmin  32638  poseq  32649  wzel  32665  wsuclem  32666  wsuclb  32669  elno2  32715  sltval2  32717  noreson  32721  sltres  32723  noseponlem  32725  nolesgn2o  32732  nodense  32750  nosupfv  32760  nosupres  32761  nosupbnd1lem3  32764  nosupbnd1lem5  32766  nosupbnd2lem1  32769  noetalem3  32773  noetalem5  32775  imagesset  32968  fvtransport  33047  brcolinear  33074  brsegle  33123  seglerflx  33127  seglemin  33128  btwnsegle  33132  fvray  33156  fvline  33159  hilbert1.1  33169  elhf2  33190  0hf  33192  nn0prpwlem  33224  nn0prpw  33225  fness  33251  fneref  33252  fnessref  33259  refssfne  33260  neibastop2lem  33262  fnemeet1  33268  tailfb  33279  filnetlem4  33283  limsucncmpi  33346  taupilemrplb  34078  relowlssretop  34121  rdgellim  34134  matunitlindflem2  34366  ptrecube  34369  poimirlem4  34373  poimirlem17  34386  poimirlem20  34389  poimirlem23  34392  poimirlem24  34393  poimirlem26  34395  poimirlem27  34396  poimirlem29  34398  poimirlem32  34401  heicant  34404  mblfinlem1  34406  mblfinlem2  34407  mblfinlem3  34408  mblfinlem4  34409  ismblfin  34410  volsupnfl  34414  itg2addnclem  34420  itg2addnclem3  34422  itg2addnc  34423  ftc1anclem5  34448  unirep  34466  cover2  34467  indexa  34486  frinfm  34488  sdclem1  34496  fdc  34498  incsequz  34501  caushft  34514  istotbnd3  34527  0totbnd  34529  sstotbnd2  34530  sstotbnd  34531  sstotbnd3  34532  isbnd3  34540  ssbnd  34544  equivbnd  34546  prdsbnd  34549  prdstotbnd  34550  cntotbnd  34552  heibor1lem  34565  heiborlem1  34567  heiborlem3  34569  heiborlem6  34572  heiborlem8  34574  bfplem2  34579  rrncmslem  34588  iccbnd  34596  opidonOLD  34608  exidres  34634  isrngod  34654  isgrpda  34711  isdrngo2  34714  igenval  34817  igenidl  34819  prtlem10  35482  lshpnel2N  35602  lsmsat  35625  lssatomic  35628  lcvnbtwn  35642  lfl1  35687  eqlkr  35716  lshpkrlem1  35727  lshpkrex  35735  cvrcon3b  35894  cvrat4  36060  3dim3  36086  ps-2  36095  llni  36125  llnle  36135  lplni  36149  lplnle  36157  lplnexllnN  36181  lvoli  36192  lnatexN  36396  elpaddn0  36417  pclfinN  36517  lhprelat3N  36657  4atexlemex2  36688  4atex  36693  4atex2-0aOLDN  36695  4atex2-0cOLDN  36697  lautcvr  36709  cdleme0ex1N  36840  cdleme50rnlem  37161  cdleme50ex  37176  cdlemg1cex  37205  cdlemkid5  37552  cdlemk  37591  tendoex  37592  cdleml5N  37597  cdlemm10N  37735  dih1dimatlem0  37945  dihjat1lem  38045  dvh3dim2  38065  dvh3dim3N  38066  dochkr1  38095  dochkr1OLDN  38096  lcfrvalsnN  38158  lcfrlem27  38186  lcfrlem37  38196  lcfr  38202  mapd1o  38265  mapdpglem23  38311  hdmap11lem2  38459  resubeu  38680  nacsfix  38744  mzpcompact2lem  38783  eldioph  38790  diophrw  38791  diophin  38805  rexrabdioph  38827  rexzrexnn0  38837  eldioph4b  38844  rencldnfilem  38853  irrapxlem5  38859  irrapxlem6  38860  pell1234qrdich  38894  pell14qrdich  38902  infmrgelbi  38911  pellqrex  38912  pellfundre  38914  pellfundlb  38917  rmxynorm  38951  congrep  39006  acongrep  39013  jm2.27  39041  fnwe2lem2  39087  islssfgi  39108  hbtlem2  39160  hbtlem4  39162  hbtlem5  39164  dgraaub  39184  mpaaeu  39186  aaitgo  39198  rgspnval  39204  rgspncl  39205  clsk1independent  39832  elabrexg  40794  restuni3  40877  iinssd  40889  founiiun  40928  wessf1ornlem  40938  founiiun0  40944  unirnmap  40964  dstregt0  41041  uzfissfz  41088  fiminre2  41140  rpgtrecnn  41143  rexabslelem  41188  infrnmptle  41193  infxrunb3rnmpt  41198  infxrpnf  41217  supminfxr  41236  iooiinicc  41314  iooiinioc  41328  uzubioo  41339  climsuse  41385  islptre  41396  climinf3  41493  limsupmnfuzlem  41503  limsupre3lem  41509  limsupre3uzlem  41512  0cnv  41519  liminfreuzlem  41579  cnrefiisplem  41606  icccncfext  41665  cncficcgt0  41666  dvbdfbdioo  41710  ioodvbdlimc1lem1  41711  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  stoweidlem9  41790  stoweidlem14  41795  stoweidlem18  41799  stoweidlem21  41802  stoweidlem29  41810  stoweidlem34  41815  stoweidlem35  41816  stoweidlem39  41820  stoweidlem41  41822  stoweidlem45  41826  stoweidlem52  41833  stoweidlem55  41836  stoweidlem57  41838  stoweidlem60  41841  stirlinglem5  41859  stirlinglem13  41867  stirlinglem14  41868  fourierdlem16  41904  fourierdlem20  41908  fourierdlem21  41909  fourierdlem22  41910  fourierdlem25  41913  fourierdlem31  41919  fourierdlem39  41927  fourierdlem41  41929  fourierdlem42  41930  fourierdlem47  41934  fourierdlem48  41935  fourierdlem49  41936  fourierdlem51  41938  fourierdlem63  41950  fourierdlem64  41951  fourierdlem65  41952  fourierdlem77  41964  fourierdlem81  41968  fourierdlem83  41970  fourierdlem103  41990  fourierdlem104  41991  elaa2lem  42014  etransclem47  42062  qndenserrnbl  42076  ioorrnopnlem  42085  ioorrnopnxrlem  42087  intsaluni  42108  salgencntex  42122  subsaliuncllem  42136  sge0resplit  42184  sge0seq  42224  sge0reuz  42225  nnfoctbdjlem  42233  meaiininclem  42264  hoicvrrex  42334  ovnlecvr  42336  ovnlerp  42340  hoidmv1lelem2  42370  hoidmvlelem2  42374  hoidmvlelem3  42375  ovnhoilem1  42379  ovnlecvr2  42388  hoiqssbl  42403  ovolval4lem2  42428  ovolval5lem2  42431  ovnovollem1  42434  ovnovollem2  42435  iinhoiicclem  42451  smfinflem  42587  smflimsuplem7  42596  sprsymrelfolem2  43091  perfectALTV  43324  9gbo  43375  11gbo  43376  nnsum3primes4  43389  nnsum3primesprm  43391  ssnn0ssfz  43829  lincsumcl  43920  lincscmcl  43921  zlmodzxzldep  43993  ldepsnlinc  43997  line2ylem  44173  line2xlem  44175  aacllem  44336