Theorem rspccv 3573

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  elinti  4911  trss  5215  fvn0ssdmfun  7019  dff3  7045  2fvcoidd  7243  ofrval  7634  limsuc  7791  limuni3  7794  peano5  7835  frxp  8068  smo11  8296  odi  8506  supub  9362  suplub  9363  elirrvOLD  9503  dfom3  9556  noinfep  9569  tcrank  9796  alephle  9998  dfac5lem5  10037  dfac2b  10041  cofsmo  10179  coftr  10183  infpssrlem4  10216  isf34lem6  10290  axcc2lem  10346  domtriomlem  10352  axdc2lem  10358  axdc3lem2  10361  axdc4lem  10365  ac5b  10388  zorn2lem2  10407  zorn2lem6  10411  pwcfsdom  10494  inar1  10686  grupw  10706  grupr  10708  gruurn  10709  grothpw  10737  grothpwex  10738  axgroth6  10739  grothomex  10740  nqereu  10840  supsrlem  11022  axpre-sup  11080  dedekind  11296  dedekindle  11297  supmullem1  12112  supmul  12114  peano5nni  12148  dfnn2  12158  peano5uzi  12581  zindd  12593  lcmfdvds  16569  lcmfunsn  16571  1arith  16855  ramcl  16957  clatleglb  18441  pslem  18495  cyccom  19132  rngisomring1  20404  psgndiflemA  21556  eqcoe1ply1eq  22243  mvmumamul1  22498  smadiadetlem0  22605  chpscmat  22786  basis2  22895  tg2  22909  clsndisj  23019  cnpimaex  23200  t1sncld  23270  regsep  23278  nrmsep3  23299  cmpsub  23344  2ndc1stc  23395  refssex  23455  ptfinfin  23463  txcnpi  23552  txcmplem1  23585  tx1stc  23594  filss  23797  ufilss  23849  fclsopni  23959  fclsrest  23968  alexsubb  23990  alexsubALTlem2  23992  alexsubALTlem4  23994  ghmcnp  24059  qustgplem  24065  mopni  24436  metrest  24468  metcnpi  24488  metcnpi2  24489  nmolb  24661  nmoleub2lem2  25072  ovoliunlem1  25459  ovolicc2lem3  25476  mblsplit  25489  fta1b  26133  plycj  26239  plycjOLD  26241  lgamgulmlem1  26995  sqfpc  27103  ostth2lem2  27601  ostth3  27605  ltsval2  27624  nogt01o  27664  madebdayim  27884  madebdaylemlrcut  27895  precsexlem9  28211  oniso  28267  bdayons  28272  dfn0s2  28328  onsfi  28352  peano5uzs  28400  bdaypw2n0bndlem  28459  vdiscusgr  29605  0vtxrusgr  29651  rusgrnumwrdl2  29660  ewlkinedg  29678  eupthseg  30281  upgreupthseg  30284  numclwwlk1  30436  l2p  30554  lpni  30555  nvz  30744  chcompl  31317  ocin  31371  hmopidmchi  32226  dmdmd  32375  dmdbr5  32383  mdsl1i  32396  sigaclci  34289  bnj23  34874  kur14lem9  35408  sconnpht  35423  cvmsdisj  35464  sat1el2xp  35573  untelirr  35902  untsucf  35904  dfon2lem4  35978  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  dfon2  35984  fwddifnp1  36359  domalom  37609  pibt2  37622  poimirlem18  37839  poimirlem21  37842  heibor1lem  38010  heiborlem4  38015  heiborlem6  38017  atlex  39576  psubspi  40007  elpcliN  40153  ldilval  40373  trlord  40829  tendotp  41021  hdmapval2  42092  cantnfresb  43566  pwelg  43801  gneispace0nelrn2  44382  gneispaceel2  44385  gneispacess2  44387  stoweid  46307  iccpartimp  47663  iccpartltu  47671  iccpartgtl  47672  iccpartleu  47674  iccpartgel  47675  isuspgrim0  48140  gricushgr  48163  1arymaptf1  48888