Theorem rspccv 3580

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  elinti  4923  trss  5230  fvn0ssdmfun  7073  dff3  7099  2fvcoidd  7301  ofrval  7692  limsuc  7847  limuni3  7850  peano5  7892  frxp  8124  smo11  8353  odi  8566  supub  9422  suplub  9423  elirrvOLDOLD  9564  dfom3  9619  noinfep  9632  tcrank  9859  alephle  10084  dfac5lem5  10123  dfac2b  10126  cofsmo  10264  coftr  10268  infpssrlem4  10301  isf34lem6  10375  axcc2lem  10431  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc4lem  10450  ac5b  10473  zorn2lem2  10492  zorn2lem6  10496  pwcfsdom  10579  inar1  10771  grupw  10791  grupr  10793  gruurn  10794  grothpw  10822  grothpwex  10823  axgroth6  10824  grothomex  10825  nqereu  10925  supsrlem  11107  axpre-sup  11165  dedekind  11384  dedekindle  11385  supmullem1  12196  supmul  12198  peano5nni  12247  dfnn2  12257  peano5uzi  12697  zindd  12709  lcmfdvds  16718  lcmfunsn  16720  1arith  17005  ramcl  17107  clatleglb  18592  pslem  18646  cyccom  19298  rngisomring1  20576  isdrng3lem2  20882  psgndiflemA  21781  eqcoe1ply1eq  22489  mvmumamul1  22741  smadiadetlem0  22848  chpscmat  23029  basis2  23138  tg2  23152  clsndisj  23262  cnpimaex  23443  t1sncld  23513  regsep  23521  nrmsep3  23542  cmpsub  23587  2ndc1stc  23638  refssex  23699  ptfinfin  23707  txcnpi  23796  txcmplem1  23829  tx1stc  23838  filss  24041  ufilss  24093  fclsopni  24203  fclsrest  24212  alexsubb  24234  alexsubALTlem2  24236  alexsubALTlem4  24238  ghmcnp  24303  qustgplem  24309  mopni  24680  metrest  24712  metcnpi  24732  metcnpi2  24733  nmolb  24905  nmoleub2lem2  25306  ovoliunlem1  25692  ovolicc2lem3  25709  mblsplit  25722  fta1b  26360  plycj  26465  plycjOLD  26467  lgamgulmlem1  27224  sqfpc  27332  ostth2lem2  27829  ostth3  27833  ltsval2  27851  nogt01o  27891  madebdayim  28112  madebdaylemlrcut  28123  precsexlem9  28439  oniso  28495  bdayons  28500  dfn0s2  28556  onsfi  28580  peano5uzs  28628  bdaypw2n0bndlem  28687  vdiscusgr  29915  0vtxrusgr  29961  rusgrnumwrdl2  29970  ewlkinedg  29988  eupthseg  30604  upgreupthseg  30607  numclwwlk1  30759  l2p  30878  lpni  30879  nvz  31068  chcompl  31641  ocin  31695  hmopidmchi  32550  dmdmd  32699  dmdbr5  32707  mdsl1i  32720  sigaclci  34562  bnj23  35148  kur14lem9  35719  sconnpht  35734  cvmsdisj  35775  sat1el2xp  35884  untelirr  36213  untsucf  36215  dfon2lem4  36289  dfon2lem6  36291  dfon2lem7  36292  dfon2lem8  36293  dfon2  36295  fwddifnp1  36670  domalom  38083  pibt2  38096  poimirlem18  38322  poimirlem21  38325  heibor1lem  38493  heiborlem4  38498  heiborlem6  38500  atlex  40123  psubspi  40554  elpcliN  40700  ldilval  40920  trlord  41376  tendotp  41568  hdmapval2  42639  cantnfresb  44084  pwelg  44319  gneispace0nelrn2  44900  gneispaceel2  44903  gneispacess2  44905  stoweid  46810  iccpartimp  48199  iccpartltu  48207  iccpartgtl  48208  iccpartleu  48210  iccpartgel  48211  isuspgrim0  48692  gricushgr  48715  1arymaptf1  49455