Theorem rspccv 3577

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  elinti  4921  trss  5228  fvn0ssdmfun  7106  dff3  7132  2fvcoidd  7336  ofrval  7737  limsuc  7894  limuni3  7897  peano5  7939  frxp  8175  smo11  8410  odi  8625  supub  9488  suplub  9489  elirrvOLDOLD  9630  dfom3  9685  noinfep  9698  tcrank  9938  alephle  10206  dfac5lem5  10245  dfac2b  10248  cofsmo  10386  coftr  10390  infpssrlem4  10423  isf34lem6  10497  axcc2lem  10553  domtriomlem  10559  axdc2lem  10565  axdc3lem2  10568  axdc4lem  10572  ac5b  10595  zorn2lem2  10614  zorn2lem6  10618  pwcfsdom  10707  inar1  10899  grupw  10919  grupr  10921  gruurn  10922  grothpw  10950  grothpwex  10951  axgroth6  10952  grothomex  10953  nqereu  11053  supsrlem  11235  axpre-sup  11293  dedekind  11512  dedekindle  11513  supmullem1  12327  supmul  12329  peano5nni  12378  dfnn2  12388  peano5uzi  12828  zindd  12840  lcmfdvds  16861  lcmfunsn  16863  1arith  17149  ramcl  17251  clatleglb  18742  pslem  18796  cyccom  19468  rngisomring1  20749  isdrng3lem2  21057  psgndiflemA  21962  eqcoe1ply1eq  22672  mvmumamul1  22924  smadiadetlem0  23031  chpscmat  23215  basis2  23324  tg2  23338  clsndisj  23448  cnpimaex  23629  t1sncld  23699  regsep  23707  nrmsep3  23728  cmpsub  23773  2ndc1stc  23824  refssex  23885  ptfinfin  23893  txcnpi  23982  txcmplem1  24015  tx1stc  24024  filss  24227  ufilss  24279  fclsopni  24389  fclsrest  24398  alexsubb  24420  alexsubALTlem2  24422  alexsubALTlem4  24424  ghmcnp  24489  qustgplem  24495  mopni  24866  metrest  24898  metcnpi  24918  metcnpi2  24919  nmolb  25091  nmoleub2lem2  25492  ovoliunlem1  25878  ovolicc2lem3  25895  mblsplit  25908  fta1b  26545  plycj  26651  lgamgulmlem1  27413  sqfpc  27521  ostth2lem2  28018  ostth3  28022  ltsval2  28070  nogt01o  28110  madebdayim  28331  madebdaylemlrcut  28342  precsexlem9  28658  oniso  28714  bdayons  28719  dfn0s2  28775  onsfi  28799  peano5uzs  28847  bdaypw2n0bndlem  28906  vdiscusgr  30169  0vtxrusgr  30215  rusgrnumwrdl2  30224  ewlkinedg  30242  eupthseg  30864  upgreupthseg  30867  numclwwlk1  31019  l2p  31138  lpni  31139  nvz  31328  chcompl  31901  ocin  31955  hmopidmchi  32810  dmdmd  32959  dmdbr5  32967  mdsl1i  32980  sigaclci  34875  bnj23  35460  kur14lem9  36187  sconnpht  36202  cvmsdisj  36243  sat1el2xp  36352  untelirr  36688  untsucf  36690  dfon2lem4  36763  dfon2lem6  36765  dfon2lem7  36766  dfon2lem8  36767  dfon2  36769  fwddifnp1  37145  domalom  38595  pibt2  38608  poimirlem18  38824  poimirlem21  38827  heibor1lem  39009  heiborlem4  39014  heiborlem6  39016  atlex  40639  psubspi  41070  elpcliN  41216  ldilval  41436  trlord  41892  tendotp  42084  hdmapval2  43155  cantnfresb  44587  pwelg  44822  gneispace0nelrn2  45402  gneispaceel2  45405  gneispacess2  45407  stoweid  47346  iccpartimp  48772  iccpartltu  48780  iccpartgtl  48781  iccpartleu  48783  iccpartgel  48784  isuspgrim0  49265  gricushgr  49288  1arymaptf1  50085