Theorem rspccv 3561

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  elinti  4898  trss  5202  fvn0ssdmfun  7026  dff3  7052  2fvcoidd  7252  ofrval  7643  limsuc  7800  limuni3  7803  peano5  7844  frxp  8076  smo11  8304  odi  8514  supub  9372  suplub  9373  elirrvOLD  9513  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  11309  dedekindle  11310  supmullem1  12126  supmul  12128  peano5nni  12177  dfnn2  12187  peano5uzi  12618  zindd  12630  lcmfdvds  16611  lcmfunsn  16613  1arith  16898  ramcl  17000  clatleglb  18484  pslem  18538  cyccom  19178  rngisomring1  20448  psgndiflemA  21581  eqcoe1ply1eq  22264  mvmumamul1  22519  smadiadetlem0  22626  chpscmat  22807  basis2  22916  tg2  22930  clsndisj  23040  cnpimaex  23221  t1sncld  23291  regsep  23299  nrmsep3  23320  cmpsub  23365  2ndc1stc  23416  refssex  23476  ptfinfin  23484  txcnpi  23573  txcmplem1  23606  tx1stc  23615  filss  23818  ufilss  23870  fclsopni  23980  fclsrest  23989  alexsubb  24011  alexsubALTlem2  24013  alexsubALTlem4  24015  ghmcnp  24080  qustgplem  24086  mopni  24457  metrest  24489  metcnpi  24509  metcnpi2  24510  nmolb  24682  nmoleub2lem2  25083  ovoliunlem1  25469  ovolicc2lem3  25486  mblsplit  25499  fta1b  26137  plycj  26242  plycjOLD  26244  lgamgulmlem1  26992  sqfpc  27100  ostth2lem2  27597  ostth3  27601  ltsval2  27620  nogt01o  27660  madebdayim  27880  madebdaylemlrcut  27891  precsexlem9  28207  oniso  28263  bdayons  28268  dfn0s2  28324  onsfi  28348  peano5uzs  28396  bdaypw2n0bndlem  28455  vdiscusgr  29600  0vtxrusgr  29646  rusgrnumwrdl2  29655  ewlkinedg  29673  eupthseg  30276  upgreupthseg  30279  numclwwlk1  30431  l2p  30550  lpni  30551  nvz  30740  chcompl  31313  ocin  31367  hmopidmchi  32222  dmdmd  32371  dmdbr5  32379  mdsl1i  32392  sigaclci  34276  bnj23  34861  kur14lem9  35396  sconnpht  35411  cvmsdisj  35452  sat1el2xp  35561  untelirr  35890  untsucf  35892  dfon2lem4  35966  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon2  35972  fwddifnp1  36347  domalom  37720  pibt2  37733  poimirlem18  37959  poimirlem21  37962  heibor1lem  38130  heiborlem4  38135  heiborlem6  38137  atlex  39762  psubspi  40193  elpcliN  40339  ldilval  40559  trlord  41015  tendotp  41207  hdmapval2  42278  cantnfresb  43752  pwelg  43987  gneispace0nelrn2  44568  gneispaceel2  44571  gneispacess2  44573  stoweid  46491  iccpartimp  47877  iccpartltu  47885  iccpartgtl  47886  iccpartleu  47888  iccpartgel  47889  isuspgrim0  48370  gricushgr  48393  1arymaptf1  49118