Theorem rspccv 3301

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1481   ∈ wcel 1988  ∀wral 2909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197

This theorem is referenced by:  ssdifsn  4309  elinti  4476  trss  4752  fvn0ssdmfun  6336  dff3  6358  2fvcoidd  6537  ofrval  6892  limsuc  7034  limuni3  7037  frxp  7272  wfrdmcl  7408  smo11  7446  odi  7644  supub  8350  suplub  8351  elirrv  8489  dfom3  8529  noinfep  8542  oemapvali  8566  tcrank  8732  infxpenlem  8821  alephle  8896  dfac5lem5  8935  dfac2  8938  cofsmo  9076  coftr  9080  infpssrlem4  9113  isf34lem6  9187  axcc2lem  9243  domtriomlem  9249  axdc2lem  9255  axdc3lem2  9258  axdc4lem  9262  ac5b  9285  zorn2lem2  9304  zorn2lem6  9308  pwcfsdom  9390  inar1  9582  grupw  9602  grupr  9604  gruurn  9605  grothpw  9633  grothpwex  9634  axgroth6  9635  grothomex  9636  nqereu  9736  supsrlem  9917  axpre-sup  9975  dedekind  10185  dedekindle  10186  supmullem1  10978  supmul  10980  peano5nni  11008  dfnn2  11018  peano5uzi  11451  zindd  11463  1arith  15612  ramcl  15714  clatleglb  17107  pslem  17187  cygabl  18273  eqcoe1ply1eq  19648  psgndiflemA  19928  mvmumamul1  20341  smadiadetlem0  20448  chpscmat  20628  basis2  20736  tg2  20750  clsndisj  20860  cnpimaex  21041  t1sncld  21111  regsep  21119  nrmsep3  21140  cmpsub  21184  2ndc1stc  21235  refssex  21295  ptfinfin  21303  txcnpi  21392  txcmplem1  21425  tx1stc  21434  filss  21638  ufilss  21690  fclsopni  21800  fclsrest  21809  alexsubb  21831  alexsubALTlem2  21833  alexsubALTlem4  21835  ghmcnp  21899  qustgplem  21905  mopni  22278  metrest  22310  metcnpi  22330  metcnpi2  22331  cfilucfil  22345  nmolb  22502  nmoleub2lem2  22897  ovoliunlem1  23251  ovolicc2lem3  23268  mblsplit  23281  fta1b  23910  plycj  24014  mtest  24139  lgamgulmlem1  24736  sqfpc  24844  ostth2lem2  25304  ostth3  25308  nbgrnself2  26240  vdiscusgr  26408  rusgrnumwrdl2  26463  ewlkinedg  26481  numclwwlk1  27202  l2p  27301  lpni  27302  nvz  27494  ubthlem2  27697  chcompl  28069  ocin  28125  hmopidmchi  28980  dmdmd  29129  dmdbr5  29137  mdsl1i  29150  sigaclci  30169  bnj23  30758  kur14lem9  31170  sconnpht  31185  cvmsdisj  31226  untelirr  31559  untsucf  31561  dfon2lem4  31665  dfon2lem6  31667  dfon2lem7  31668  dfon2lem8  31669  dfon2  31671  frrlem5e  31762  sltval2  31783  fwddifnp1  32247  poimirlem18  33398  poimirlem21  33401  heibor1lem  33579  heiborlem4  33584  heiborlem6  33586  atlex  34422  psubspi  34852  elpcliN  34998  ldilval  35218  trlord  35676  tendotp  35868  hdmapval2  36943  pwelg  37684  gneispace0nelrn2  38259  gneispaceel2  38262  gneispacess2  38264  stoweid  40043  iccpartltu  41125  iccpartgtl  41126  iccpartleu  41128  iccpartgel  41129