Theorem ssralv 2104

Description: Quantification restricted to a subclass.

Assertion

Ref	Expression
ssralv	|- (A (_ B -> (A.x e. B ph -> A.x e. A ph))

Distinct variable groups:   x,A   x,B

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 2053	. . 3 |- (A (_ B -> (x e. A -> x e. B))
2	1	imim1d 28	. 2 |- (A (_ B -> ((x e. B -> ph) -> (x e. A -> ph)))
3	2	r19.20dv2 1703	1 |- (A (_ B -> (A.x e. B ph -> A.x e. A ph))

Syntax hints:   -> wi 3   e. wcel 955  A.wral 1637   (_ wss 2037

This theorem is referenced by:  unifi 4532  cvg3 6860  clm4le 7019  clm0 7021  clmi1 7024  clm4at 7028  climfnn 7030  2climnn 7039  2climnn0 7040  iserzcmp 7078  rescncf 7207  eirrlem2 7331  eirrlem5 7334  metreslem 7762  metcnss2 7838  occllem6 9094  projlem25 9126  projlem26 9127  cnrscoa 10397

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ral 1641  df-in 2041  df-ss 2043

Copyright terms: Public domain