Theorem ssralv 2114

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 2063	. . 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 1711	1 |- (A (_ B -> (A.x e. B ph -> A.x e. A ph))

Syntax hints:   -> wi 3   e. wcel 958  A.wral 1645   (_ wss 2047

This theorem is referenced by:  unifiOLD 4557  cvg3 6923  clm4le 7081  clm0 7083  clmi1 7086  clm4at 7090  climfnn 7092  2climnn 7102  2climnn0 7103  iserzcmp 7142  rescncf 7272  eirrlem2 7390  eirrlem5 7393  metreslem 7822  metcnss2 7899  occllem6 9178  projlem25 9210  projlem26 9211  cnrscoa 10510

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-in 2051  df-ss 2053

Copyright terms: Public domain