Theorem rspccv 3457

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)

Hypothesis

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

Assertion

Ref	Expression
rspccv	⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

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

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccv

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3456	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 32	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631   ∈ wcel 2145  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353

This theorem is referenced by:  ssdifsnOLD  4455  elinti  4620  trss  4895  fvn0ssdmfun  6493  dff3  6515  2fvcoidd  6695  ofrval  7054  limsuc  7196  limuni3  7199  frxp  7438  wfrdmcl  7576  smo11  7614  odi  7813  supub  8521  suplub  8522  elirrv  8657  dfom3  8708  noinfep  8721  tcrank  8911  alephle  9111  dfac5lem5  9150  dfac2b  9153  dfac2OLD  9155  cofsmo  9293  coftr  9297  infpssrlem4  9330  isf34lem6  9404  axcc2lem  9460  domtriomlem  9466  axdc2lem  9472  axdc3lem2  9475  axdc4lem  9479  ac5b  9502  zorn2lem2  9521  zorn2lem6  9525  pwcfsdom  9607  inar1  9799  grupw  9819  grupr  9821  gruurn  9822  grothpw  9850  grothpwex  9851  axgroth6  9852  grothomex  9853  nqereu  9953  supsrlem  10134  axpre-sup  10192  dedekind  10402  dedekindle  10403  supmullem1  11195  supmul  11197  peano5nni  11225  dfnn2  11235  peano5uzi  11668  zindd  11680  1arith  15838  ramcl  15940  clatleglb  17334  pslem  17414  cygabl  18499  eqcoe1ply1eq  19882  psgndiflemA  20163  mvmumamul1  20578  smadiadetlem0  20686  chpscmat  20867  basis2  20976  tg2  20990  clsndisj  21100  cnpimaex  21281  t1sncld  21351  regsep  21359  nrmsep3  21380  cmpsub  21424  2ndc1stc  21475  refssex  21535  ptfinfin  21543  txcnpi  21632  txcmplem1  21665  tx1stc  21674  filss  21877  ufilss  21929  fclsopni  22039  fclsrest  22048  alexsubb  22070  alexsubALTlem2  22072  alexsubALTlem4  22074  ghmcnp  22138  qustgplem  22144  mopni  22517  metrest  22549  metcnpi  22569  metcnpi2  22570  nmolb  22741  nmoleub2lem2  23135  ovoliunlem1  23490  ovolicc2lem3  23507  mblsplit  23520  fta1b  24149  plycj  24253  lgamgulmlem1  24976  sqfpc  25084  ostth2lem2  25544  ostth3  25548  nbgrnself2OLD  26482  vdiscusgr  26662  rusgrnumwrdl2  26717  ewlkinedg  26735  numclwwlk1  27548  l2p  27673  lpni  27674  nvz  27864  chcompl  28439  ocin  28495  hmopidmchi  29350  dmdmd  29499  dmdbr5  29507  mdsl1i  29520  sigaclci  30535  bnj23  31124  kur14lem9  31534  sconnpht  31549  cvmsdisj  31590  untelirr  31923  untsucf  31925  dfon2lem4  32027  dfon2lem6  32029  dfon2lem7  32030  dfon2lem8  32031  dfon2  32033  frrlem5e  32125  sltval2  32146  fwddifnp1  32609  poimirlem18  33760  poimirlem21  33763  heibor1lem  33940  heiborlem4  33945  heiborlem6  33947  atlex  35125  psubspi  35555  elpcliN  35701  ldilval  35921  trlord  36378  tendotp  36570  hdmapval2  37642  pwelg  38391  gneispace0nelrn2  38965  gneispaceel2  38968  gneispacess2  38970  stoweid  40797  iccpartltu  41889  iccpartgtl  41890  iccpartleu  41892  iccpartgel  41893