Theorem ssralv 3244

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 3174	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 75	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 2564	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2164  ∀wral 2472   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-ral 2477  df-in 3160  df-ss 3167

This theorem is referenced by:  iinss1  3925  poss  4330  sess2  4370  trssord  4412  funco  5295  funimaexglem  5338  isores3  5859  isoini2  5863  smores  6347  smores2  6349  tfrlem5  6369  resixp  6789  ac6sfi  6956  difinfinf  7162  peano5nnnn  7954  peano5nni  8987  caucvgre  11128  rexanuz  11135  cau3lem  11261  isumclim3  11569  fsumiun  11623  pcfac  12491  ctinf  12590  strsetsid  12654  imasaddfnlemg  12900  tgcn  14387  tgcnp  14388  cnss2  14406  cncnp  14409  sslm  14426  metrest  14685  rescncf  14760  suplociccex  14804  limcresi  14845  nninfsellemeq  15574