Theorem rabssdv 3890

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.)

Hypothesis

Ref	Expression
rabssdv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
rabssdv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rabssdv

Step	Hyp	Ref	Expression
1		rabssdv.1	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵)
2	1	3exp 1141	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝑥 ∈ 𝐵)))
3	2	ralrimiv 3164	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵))
4		rabss 3887	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵))
5	3, 4	sylibr 225	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1100   ∈ wcel 2157  ∀wral 3107  {crab 3111   ⊆ wss 3780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rab 3116  df-in 3787  df-ss 3794

This theorem is referenced by:  suppss2  7574  oemapvali  8838  cantnflem1  8843  harval2  9116  zsupss  12016  ramub1lem1  15967  symggen  18111  efgsfo  18373  ablfacrp  18687  ablfac1eu  18694  pgpfac1lem5  18700  ablfaclem3  18708  nrmr0reg  21787  ptcmplem3  22092  abelthlem2  24423  lgamgulmlem1  24992  neibastop2lem  32698  topmeet  32702  cntotbnd  33925  mapdrvallem2  37444  k0004ss1  38967  liminfvalxr  40513