Theorem rspccv 3577

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079

This theorem is used by:  elinti  4920  trss  5227  fvn0ssdmfun  7069  dff3  7095  2fvcoidd  7295  ofrval  7688  limsuc  7843  limuni3  7846  peano5  7888  frxp  8120  smo11  8349  odi  8562  supub  9417  suplub  9418  elirrvOLDOLD  9559  dfom3  9614  noinfep  9627  tcrank  9854  alephle  10079  dfac5lem5  10118  dfac2b  10121  cofsmo  10259  coftr  10263  infpssrlem4  10296  isf34lem6  10370  axcc2lem  10426  domtriomlem  10432  axdc2lem  10438  axdc3lem2  10441  axdc4lem  10445  ac5b  10468  zorn2lem2  10487  zorn2lem6  10491  pwcfsdom  10574  inar1  10766  grupw  10786  grupr  10788  gruurn  10789  grothpw  10817  grothpwex  10818  axgroth6  10819  grothomex  10820  nqereu  10920  supsrlem  11102  axpre-sup  11160  dedekind  11379  dedekindle  11380  supmullem1  12191  supmul  12193  peano5nni  12242  dfnn2  12252  peano5uzi  12691  zindd  12703  lcmfdvds  16706  lcmfunsn  16708  1arith  16993  ramcl  17095  clatleglb  18580  pslem  18634  cyccom  19280  rngisomring1  20557  isdrng3lem2  20863  psgndiflemA  21762  eqcoe1ply1eq  22470  mvmumamul1  22722  smadiadetlem0  22829  chpscmat  23010  basis2  23119  tg2  23133  clsndisj  23243  cnpimaex  23424  t1sncld  23494  regsep  23502  nrmsep3  23523  cmpsub  23568  2ndc1stc  23619  refssex  23679  ptfinfin  23687  txcnpi  23776  txcmplem1  23809  tx1stc  23818  filss  24021  ufilss  24073  fclsopni  24183  fclsrest  24192  alexsubb  24214  alexsubALTlem2  24216  alexsubALTlem4  24218  ghmcnp  24283  qustgplem  24289  mopni  24660  metrest  24692  metcnpi  24712  metcnpi2  24713  nmolb  24885  nmoleub2lem2  25286  ovoliunlem1  25672  ovolicc2lem3  25689  mblsplit  25702  fta1b  26340  plycj  26445  plycjOLD  26447  lgamgulmlem1  27204  sqfpc  27312  ostth2lem2  27809  ostth3  27813  ltsval2  27831  nogt01o  27871  madebdayim  28092  madebdaylemlrcut  28103  precsexlem9  28419  oniso  28475  bdayons  28480  dfn0s2  28536  onsfi  28560  peano5uzs  28608  bdaypw2n0bndlem  28667  vdiscusgr  29892  0vtxrusgr  29938  rusgrnumwrdl2  29947  ewlkinedg  29965  eupthseg  30568  upgreupthseg  30571  numclwwlk1  30723  l2p  30842  lpni  30843  nvz  31032  chcompl  31605  ocin  31659  hmopidmchi  32514  dmdmd  32663  dmdbr5  32671  mdsl1i  32684  sigaclci  34531  bnj23  35116  kur14lem9  35714  sconnpht  35729  cvmsdisj  35770  sat1el2xp  35879  untelirr  36208  untsucf  36210  dfon2lem4  36284  dfon2lem6  36286  dfon2lem7  36287  dfon2lem8  36288  dfon2  36290  fwddifnp1  36665  domalom  38078  pibt2  38091  poimirlem18  38317  poimirlem21  38320  heibor1lem  38488  heiborlem4  38493  heiborlem6  38495  atlex  40118  psubspi  40549  elpcliN  40695  ldilval  40915  trlord  41371  tendotp  41563  hdmapval2  42634  cantnfresb  44079  pwelg  44314  gneispace0nelrn2  44895  gneispaceel2  44898  gneispacess2  44900  stoweid  46805  iccpartimp  48194  iccpartltu  48202  iccpartgtl  48203  iccpartleu  48205  iccpartgel  48206  isuspgrim0  48687  gricushgr  48710  1arymaptf1  49450