Theorem rspccv 3575

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  elinti  4913  trss  5217  fvn0ssdmfun  7028  dff3  7054  2fvcoidd  7253  ofrval  7644  limsuc  7801  limuni3  7804  peano5  7845  frxp  8078  smo11  8306  odi  8516  supub  9374  suplub  9375  elirrvOLD  9515  dfom3  9568  noinfep  9581  tcrank  9808  alephle  10010  dfac5lem5  10049  dfac2b  10053  cofsmo  10191  coftr  10195  infpssrlem4  10228  isf34lem6  10302  axcc2lem  10358  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc4lem  10377  ac5b  10400  zorn2lem2  10419  zorn2lem6  10423  pwcfsdom  10506  inar1  10698  grupw  10718  grupr  10720  gruurn  10721  grothpw  10749  grothpwex  10750  axgroth6  10751  grothomex  10752  nqereu  10852  supsrlem  11034  axpre-sup  11092  dedekind  11308  dedekindle  11309  supmullem1  12124  supmul  12126  peano5nni  12160  dfnn2  12170  peano5uzi  12593  zindd  12605  lcmfdvds  16581  lcmfunsn  16583  1arith  16867  ramcl  16969  clatleglb  18453  pslem  18507  cyccom  19144  rngisomring1  20416  psgndiflemA  21568  eqcoe1ply1eq  22255  mvmumamul1  22510  smadiadetlem0  22617  chpscmat  22798  basis2  22907  tg2  22921  clsndisj  23031  cnpimaex  23212  t1sncld  23282  regsep  23290  nrmsep3  23311  cmpsub  23356  2ndc1stc  23407  refssex  23467  ptfinfin  23475  txcnpi  23564  txcmplem1  23597  tx1stc  23606  filss  23809  ufilss  23861  fclsopni  23971  fclsrest  23980  alexsubb  24002  alexsubALTlem2  24004  alexsubALTlem4  24006  ghmcnp  24071  qustgplem  24077  mopni  24448  metrest  24480  metcnpi  24500  metcnpi2  24501  nmolb  24673  nmoleub2lem2  25084  ovoliunlem1  25471  ovolicc2lem3  25488  mblsplit  25501  fta1b  26145  plycj  26251  plycjOLD  26253  lgamgulmlem1  27007  sqfpc  27115  ostth2lem2  27613  ostth3  27617  ltsval2  27636  nogt01o  27676  madebdayim  27896  madebdaylemlrcut  27907  precsexlem9  28223  oniso  28279  bdayons  28284  dfn0s2  28340  onsfi  28364  peano5uzs  28412  bdaypw2n0bndlem  28471  vdiscusgr  29617  0vtxrusgr  29663  rusgrnumwrdl2  29672  ewlkinedg  29690  eupthseg  30293  upgreupthseg  30296  numclwwlk1  30448  l2p  30567  lpni  30568  nvz  30757  chcompl  31330  ocin  31384  hmopidmchi  32239  dmdmd  32388  dmdbr5  32396  mdsl1i  32409  sigaclci  34310  bnj23  34895  kur14lem9  35430  sconnpht  35445  cvmsdisj  35486  sat1el2xp  35595  untelirr  35924  untsucf  35926  dfon2lem4  36000  dfon2lem6  36002  dfon2lem7  36003  dfon2lem8  36004  dfon2  36006  fwddifnp1  36381  domalom  37659  pibt2  37672  poimirlem18  37889  poimirlem21  37892  heibor1lem  38060  heiborlem4  38065  heiborlem6  38067  atlex  39692  psubspi  40123  elpcliN  40269  ldilval  40489  trlord  40945  tendotp  41137  hdmapval2  42208  cantnfresb  43681  pwelg  43916  gneispace0nelrn2  44497  gneispaceel2  44500  gneispacess2  44502  stoweid  46421  iccpartimp  47777  iccpartltu  47785  iccpartgtl  47786  iccpartleu  47788  iccpartgel  47789  isuspgrim0  48254  gricushgr  48277  1arymaptf1  49002