Theorem ssralv 3221

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv	⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3151	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 75	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 2547	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2148  ∀wral 2455   ⊆ wss 3131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-in 3137  df-ss 3144

This theorem is referenced by:  iinss1  3900  poss  4300  sess2  4340  trssord  4382  funco  5258  funimaexglem  5301  isores3  5818  isoini2  5822  smores  6295  smores2  6297  tfrlem5  6317  resixp  6735  ac6sfi  6900  difinfinf  7102  peano5nnnn  7893  peano5nni  8924  caucvgre  10992  rexanuz  10999  cau3lem  11125  isumclim3  11433  fsumiun  11487  pcfac  12350  ctinf  12433  strsetsid  12497  imasaddfnlemg  12740  tgcn  13747  tgcnp  13748  cnss2  13766  cncnp  13769  sslm  13786  metrest  14045  rescncf  14107  suplociccex  14142  limcresi  14174  nninfsellemeq  14802