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 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  elinti  4915  trss  5221  fvn0ssdmfun  7075  dff3  7101  2fvcoidd  7306  ofrval  7706  limsuc  7861  limuni3  7864  peano5  7906  frxp  8141  smo11  8376  odi  8591  supub  9455  suplub  9456  elirrvOLDOLD  9597  dfom3  9652  noinfep  9665  tcrank  9905  alephle  10171  dfac5lem5  10210  dfac2b  10213  cofsmo  10351  coftr  10355  infpssrlem4  10388  isf34lem6  10462  axcc2lem  10518  domtriomlem  10524  axdc2lem  10530  axdc3lem2  10533  axdc4lem  10537  ac5b  10560  zorn2lem2  10579  zorn2lem6  10583  pwcfsdom  10672  inar1  10864  grupw  10884  grupr  10886  gruurn  10887  grothpw  10915  grothpwex  10916  axgroth6  10917  grothomex  10918  nqereu  11018  supsrlem  11200  axpre-sup  11258  dedekind  11477  dedekindle  11478  supmullem1  12291  supmul  12293  peano5nni  12342  dfnn2  12352  peano5uzi  12792  zindd  12804  lcmfdvds  16823  lcmfunsn  16825  1arith  17111  ramcl  17213  clatleglb  18698  pslem  18752  cyccom  19424  rngisomring1  20704  isdrng3lem2  21012  psgndiflemA  21913  eqcoe1ply1eq  22623  mvmumamul1  22875  smadiadetlem0  22982  chpscmat  23166  basis2  23275  tg2  23289  clsndisj  23399  cnpimaex  23580  t1sncld  23650  regsep  23658  nrmsep3  23679  cmpsub  23724  2ndc1stc  23775  refssex  23836  ptfinfin  23844  txcnpi  23933  txcmplem1  23966  tx1stc  23975  filss  24178  ufilss  24230  fclsopni  24340  fclsrest  24349  alexsubb  24371  alexsubALTlem2  24373  alexsubALTlem4  24375  ghmcnp  24440  qustgplem  24446  mopni  24817  metrest  24849  metcnpi  24869  metcnpi2  24870  nmolb  25042  nmoleub2lem2  25443  ovoliunlem1  25829  ovolicc2lem3  25846  mblsplit  25859  fta1b  26496  plycj  26602  lgamgulmlem1  27362  sqfpc  27470  ostth2lem2  27967  ostth3  27971  ltsval2  28019  nogt01o  28059  madebdayim  28280  madebdaylemlrcut  28291  precsexlem9  28607  oniso  28663  bdayons  28668  dfn0s2  28724  onsfi  28748  peano5uzs  28796  bdaypw2n0bndlem  28855  vdiscusgr  30118  0vtxrusgr  30164  rusgrnumwrdl2  30173  ewlkinedg  30191  eupthseg  30813  upgreupthseg  30816  numclwwlk1  30968  l2p  31087  lpni  31088  nvz  31277  chcompl  31850  ocin  31904  hmopidmchi  32759  dmdmd  32908  dmdbr5  32916  mdsl1i  32929  sigaclci  34811  bnj23  35396  kur14lem9  36066  sconnpht  36081  cvmsdisj  36122  sat1el2xp  36231  untelirr  36566  untsucf  36568  dfon2lem4  36641  dfon2lem6  36643  dfon2lem7  36644  dfon2lem8  36645  dfon2  36647  fwddifnp1  37023  domalom  38421  pibt2  38434  poimirlem18  38650  poimirlem21  38653  heibor1lem  38837  heiborlem4  38842  heiborlem6  38844  atlex  40467  psubspi  40898  elpcliN  41044  ldilval  41264  trlord  41720  tendotp  41912  hdmapval2  42983  cantnfresb  44420  pwelg  44655  gneispace0nelrn2  45235  gneispaceel2  45238  gneispacess2  45240  stoweid  47167  iccpartimp  48593  iccpartltu  48601  iccpartgtl  48602  iccpartleu  48604  iccpartgel  48605  isuspgrim0  49086  gricushgr  49109  1arymaptf1  49848