Theorem rspccv 3573

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  elinti  4916  trss  5222  fvn0ssdmfun  7067  dff3  7093  2fvcoidd  7298  ofrval  7690  limsuc  7845  limuni3  7848  peano5  7890  frxp  8124  smo11  8353  odi  8566  supub  9429  suplub  9430  elirrvOLDOLD  9571  dfom3  9626  noinfep  9639  tcrank  9866  alephle  10091  dfac5lem5  10130  dfac2b  10133  cofsmo  10271  coftr  10275  infpssrlem4  10308  isf34lem6  10382  axcc2lem  10438  domtriomlem  10444  axdc2lem  10450  axdc3lem2  10453  axdc4lem  10457  ac5b  10480  zorn2lem2  10499  zorn2lem6  10503  pwcfsdom  10592  inar1  10784  grupw  10804  grupr  10806  gruurn  10807  grothpw  10835  grothpwex  10836  axgroth6  10837  grothomex  10838  nqereu  10938  supsrlem  11120  axpre-sup  11178  dedekind  11397  dedekindle  11398  supmullem1  12209  supmul  12211  peano5nni  12260  dfnn2  12270  peano5uzi  12710  zindd  12722  lcmfdvds  16732  lcmfunsn  16734  1arith  17019  ramcl  17121  clatleglb  18606  pslem  18660  cyccom  19331  rngisomring1  20609  isdrng3lem2  20915  psgndiflemA  21814  eqcoe1ply1eq  22524  mvmumamul1  22776  smadiadetlem0  22883  chpscmat  23067  basis2  23176  tg2  23190  clsndisj  23300  cnpimaex  23481  t1sncld  23551  regsep  23559  nrmsep3  23580  cmpsub  23625  2ndc1stc  23676  refssex  23737  ptfinfin  23745  txcnpi  23834  txcmplem1  23867  tx1stc  23876  filss  24079  ufilss  24131  fclsopni  24241  fclsrest  24250  alexsubb  24272  alexsubALTlem2  24274  alexsubALTlem4  24276  ghmcnp  24341  qustgplem  24347  mopni  24718  metrest  24750  metcnpi  24770  metcnpi2  24771  nmolb  24943  nmoleub2lem2  25344  ovoliunlem1  25730  ovolicc2lem3  25747  mblsplit  25760  fta1b  26397  plycj  26503  plycjOLD  26505  lgamgulmlem1  27265  sqfpc  27373  ostth2lem2  27870  ostth3  27874  ltsval2  27892  nogt01o  27932  madebdayim  28153  madebdaylemlrcut  28164  precsexlem9  28480  oniso  28536  bdayons  28541  dfn0s2  28597  onsfi  28621  peano5uzs  28669  bdaypw2n0bndlem  28728  vdiscusgr  29991  0vtxrusgr  30037  rusgrnumwrdl2  30046  ewlkinedg  30064  eupthseg  30686  upgreupthseg  30689  numclwwlk1  30841  l2p  30960  lpni  30961  nvz  31150  chcompl  31723  ocin  31777  hmopidmchi  32632  dmdmd  32781  dmdbr5  32789  mdsl1i  32802  sigaclci  34642  bnj23  35228  kur14lem9  35793  sconnpht  35808  cvmsdisj  35849  sat1el2xp  35958  untelirr  36287  untsucf  36289  dfon2lem4  36363  dfon2lem6  36365  dfon2lem7  36366  dfon2lem8  36367  dfon2  36369  fwddifnp1  36745  domalom  38158  pibt2  38171  poimirlem18  38387  poimirlem21  38390  heibor1lem  38559  heiborlem4  38564  heiborlem6  38566  atlex  40189  psubspi  40620  elpcliN  40766  ldilval  40986  trlord  41442  tendotp  41634  hdmapval2  42705  cantnfresb  44165  pwelg  44400  gneispace0nelrn2  44981  gneispaceel2  44984  gneispacess2  44986  stoweid  46891  iccpartimp  48317  iccpartltu  48325  iccpartgtl  48326  iccpartleu  48328  iccpartgel  48329  isuspgrim0  48810  gricushgr  48833  1arymaptf1  49572