Theorem rspccv 3619

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143

This theorem is referenced by:  elinti  4884  trss  5180  fvn0ssdmfun  6841  dff3  6865  2fvcoidd  7052  ofrval  7418  limsuc  7563  limuni3  7566  frxp  7819  wfrdmcl  7962  smo11  8000  odi  8204  supub  8922  suplub  8923  elirrv  9059  dfom3  9109  noinfep  9122  tcrank  9312  alephle  9513  dfac5lem5  9552  dfac2b  9555  cofsmo  9690  coftr  9694  infpssrlem4  9727  isf34lem6  9801  axcc2lem  9857  domtriomlem  9863  axdc2lem  9869  axdc3lem2  9872  axdc4lem  9876  ac5b  9899  zorn2lem2  9918  zorn2lem6  9922  pwcfsdom  10004  inar1  10196  grupw  10216  grupr  10218  gruurn  10219  grothpw  10247  grothpwex  10248  axgroth6  10249  grothomex  10250  nqereu  10350  supsrlem  10532  axpre-sup  10590  dedekind  10802  dedekindle  10803  supmullem1  11610  supmul  11612  peano5nni  11640  dfnn2  11650  peano5uzi  12070  zindd  12082  lcmfdvds  15985  lcmfunsn  15987  1arith  16262  ramcl  16364  clatleglb  17735  pslem  17815  cyccom  18345  cygablOLD  19010  eqcoe1ply1eq  20464  psgndiflemA  20744  mvmumamul1  21162  smadiadetlem0  21269  chpscmat  21449  basis2  21558  tg2  21572  clsndisj  21682  cnpimaex  21863  t1sncld  21933  regsep  21941  nrmsep3  21962  cmpsub  22007  2ndc1stc  22058  refssex  22118  ptfinfin  22126  txcnpi  22215  txcmplem1  22248  tx1stc  22257  filss  22460  ufilss  22512  fclsopni  22622  fclsrest  22631  alexsubb  22653  alexsubALTlem2  22655  alexsubALTlem4  22657  ghmcnp  22722  qustgplem  22728  mopni  23101  metrest  23133  metcnpi  23153  metcnpi2  23154  nmolb  23325  nmoleub2lem2  23719  ovoliunlem1  24102  ovolicc2lem3  24119  mblsplit  24132  fta1b  24762  plycj  24866  lgamgulmlem1  25605  sqfpc  25713  ostth2lem2  26209  ostth3  26213  vdiscusgr  27312  0vtxrusgr  27358  rusgrnumwrdl2  27367  ewlkinedg  27385  eupthseg  27984  upgreupthseg  27987  numclwwlk1  28139  l2p  28255  lpni  28256  nvz  28445  chcompl  29018  ocin  29072  hmopidmchi  29927  dmdmd  30076  dmdbr5  30084  mdsl1i  30097  sigaclci  31391  bnj23  31988  kur14lem9  32461  sconnpht  32476  cvmsdisj  32517  sat1el2xp  32626  untelirr  32934  untsucf  32936  dfon2lem4  33031  dfon2lem6  33033  dfon2lem7  33034  dfon2lem8  33035  dfon2  33037  sltval2  33163  fwddifnp1  33626  domalom  34684  pibt2  34697  poimirlem18  34909  poimirlem21  34912  heibor1lem  35086  heiborlem4  35091  heiborlem6  35093  atlex  36451  psubspi  36882  elpcliN  37028  ldilval  37248  trlord  37704  tendotp  37896  hdmapval2  38967  pwelg  39917  gneispace0nelrn2  40489  gneispaceel2  40492  gneispacess2  40494  stoweid  42347  iccpartimp  43576  iccpartltu  43584  iccpartgtl  43585  iccpartleu  43587  iccpartgel  43588  isomushgr  43990  isomuspgrlem1  43991  isomuspgr  43998  isomgrtrlem  44002