Theorem rspccv 3529

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2048  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-v 3414

This theorem is referenced by:  elinti  4756  trss  5037  fvn0ssdmfun  6665  dff3  6687  2fvcoidd  6876  ofrval  7235  limsuc  7378  limuni3  7381  frxp  7622  wfrdmcl  7764  smo11  7802  odi  8002  supub  8714  suplub  8715  elirrv  8851  dfom3  8900  noinfep  8913  tcrank  9103  alephle  9304  dfac5lem5  9343  dfac2b  9346  cofsmo  9485  coftr  9489  infpssrlem4  9522  isf34lem6  9596  axcc2lem  9652  domtriomlem  9658  axdc2lem  9664  axdc3lem2  9667  axdc4lem  9671  ac5b  9694  zorn2lem2  9713  zorn2lem6  9717  pwcfsdom  9799  inar1  9991  grupw  10011  grupr  10013  gruurn  10014  grothpw  10042  grothpwex  10043  axgroth6  10044  grothomex  10045  nqereu  10145  supsrlem  10327  axpre-sup  10385  dedekind  10599  dedekindle  10600  supmullem1  11408  supmul  11410  peano5nni  11438  dfnn2  11450  peano5uzi  11881  zindd  11893  lcmfdvds  15836  lcmfunsn  15838  1arith  16113  ramcl  16215  clatleglb  17588  pslem  17668  cygabl  18759  eqcoe1ply1eq  20162  psgndiflemA  20441  mvmumamul1  20861  smadiadetlem0  20968  chpscmat  21148  basis2  21257  tg2  21271  clsndisj  21381  cnpimaex  21562  t1sncld  21632  regsep  21640  nrmsep3  21661  cmpsub  21706  2ndc1stc  21757  refssex  21817  ptfinfin  21825  txcnpi  21914  txcmplem1  21947  tx1stc  21956  filss  22159  ufilss  22211  fclsopni  22321  fclsrest  22330  alexsubb  22352  alexsubALTlem2  22354  alexsubALTlem4  22356  ghmcnp  22420  qustgplem  22426  mopni  22799  metrest  22831  metcnpi  22851  metcnpi2  22852  nmolb  23023  nmoleub2lem2  23417  ovoliunlem1  23800  ovolicc2lem3  23817  mblsplit  23830  fta1b  24460  plycj  24564  lgamgulmlem1  25302  sqfpc  25410  ostth2lem2  25906  ostth3  25910  vdiscusgr  27010  0vtxrusgr  27056  rusgrnumwrdl2  27065  ewlkinedg  27083  eupthseg  27729  upgreupthseg  27732  numclwwlk1  27903  l2p  28027  lpni  28028  nvz  28217  chcompl  28792  ocin  28848  hmopidmchi  29703  dmdmd  29852  dmdbr5  29860  mdsl1i  29873  sigaclci  31027  bnj23  31627  kur14lem9  32036  sconnpht  32051  cvmsdisj  32092  untelirr  32424  untsucf  32426  dfon2lem4  32521  dfon2lem6  32523  dfon2lem7  32524  dfon2lem8  32525  dfon2  32527  sltval2  32654  fwddifnp1  33117  domalom  34091  pibt2  34104  poimirlem18  34329  poimirlem21  34332  heibor1lem  34507  heiborlem4  34512  heiborlem6  34514  atlex  35875  psubspi  36306  elpcliN  36452  ldilval  36672  trlord  37128  tendotp  37320  hdmapval2  38391  pwelg  39259  gneispace0nelrn2  39832  gneispaceel2  39835  gneispacess2  39837  stoweid  41758  iccpartimp  42928  iccpartltu  42936  iccpartgtl  42937  iccpartleu  42939  iccpartgel  42940  isomushgr  43333  isomuspgrlem1  43334  isomuspgr  43341  isomgrtrlem  43345