Theorem rspccv 3574

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 3573	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 33	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  elinti  4916  trss  5222  fvn0ssdmfun  7072  dff3  7098  2fvcoidd  7303  ofrval  7703  limsuc  7858  limuni3  7861  peano5  7903  frxp  8136  smo11  8365  odi  8580  supub  9444  suplub  9445  elirrvOLDOLD  9586  dfom3  9641  noinfep  9654  tcrank  9894  alephle  10160  dfac5lem5  10199  dfac2b  10202  cofsmo  10340  coftr  10344  infpssrlem4  10377  isf34lem6  10451  axcc2lem  10507  domtriomlem  10513  axdc2lem  10519  axdc3lem2  10522  axdc4lem  10526  ac5b  10549  zorn2lem2  10568  zorn2lem6  10572  pwcfsdom  10661  inar1  10853  grupw  10873  grupr  10875  gruurn  10876  grothpw  10904  grothpwex  10905  axgroth6  10906  grothomex  10907  nqereu  11007  supsrlem  11189  axpre-sup  11247  dedekind  11466  dedekindle  11467  supmullem1  12280  supmul  12282  peano5nni  12331  dfnn2  12341  peano5uzi  12781  zindd  12793  lcmfdvds  16810  lcmfunsn  16812  1arith  17098  ramcl  17200  clatleglb  18685  pslem  18739  cyccom  19411  rngisomring1  20691  isdrng3lem2  20999  psgndiflemA  21900  eqcoe1ply1eq  22610  mvmumamul1  22862  smadiadetlem0  22969  chpscmat  23153  basis2  23262  tg2  23276  clsndisj  23386  cnpimaex  23567  t1sncld  23637  regsep  23645  nrmsep3  23666  cmpsub  23711  2ndc1stc  23762  refssex  23823  ptfinfin  23831  txcnpi  23920  txcmplem1  23953  tx1stc  23962  filss  24165  ufilss  24217  fclsopni  24327  fclsrest  24336  alexsubb  24358  alexsubALTlem2  24360  alexsubALTlem4  24362  ghmcnp  24427  qustgplem  24433  mopni  24804  metrest  24836  metcnpi  24856  metcnpi2  24857  nmolb  25029  nmoleub2lem2  25430  ovoliunlem1  25816  ovolicc2lem3  25833  mblsplit  25846  fta1b  26483  plycj  26589  lgamgulmlem1  27349  sqfpc  27457  ostth2lem2  27954  ostth3  27958  ltsval2  28006  nogt01o  28046  madebdayim  28267  madebdaylemlrcut  28278  precsexlem9  28594  oniso  28650  bdayons  28655  dfn0s2  28711  onsfi  28735  peano5uzs  28783  bdaypw2n0bndlem  28842  vdiscusgr  30105  0vtxrusgr  30151  rusgrnumwrdl2  30160  ewlkinedg  30178  eupthseg  30800  upgreupthseg  30803  numclwwlk1  30955  l2p  31074  lpni  31075  nvz  31264  chcompl  31837  ocin  31891  hmopidmchi  32746  dmdmd  32895  dmdbr5  32903  mdsl1i  32916  sigaclci  34757  bnj23  35342  kur14lem9  35958  sconnpht  35973  cvmsdisj  36014  sat1el2xp  36123  untelirr  36452  untsucf  36454  dfon2lem4  36528  dfon2lem6  36530  dfon2lem7  36531  dfon2lem8  36532  dfon2  36534  fwddifnp1  36910  domalom  38307  pibt2  38320  poimirlem18  38536  poimirlem21  38539  heibor1lem  38723  heiborlem4  38728  heiborlem6  38730  atlex  40353  psubspi  40784  elpcliN  40930  ldilval  41150  trlord  41606  tendotp  41798  hdmapval2  42869  cantnfresb  44310  pwelg  44545  gneispace0nelrn2  45126  gneispaceel2  45129  gneispacess2  45131  stoweid  47042  iccpartimp  48468  iccpartltu  48476  iccpartgtl  48477  iccpartleu  48479  iccpartgel  48480  isuspgrim0  48961  gricushgr  48984  1arymaptf1  49723