Theorem rabssdv 4025

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 1137	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝑥 ∈ 𝐵)))
3	2	ralrimiv 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵))
4		rabss 4021	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵))
5	3, 4	sylibr 237	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2145  ∀wral 3078  {crab 3414   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rab 3415  df-ss 3919

This theorem is used by:  suppss2  8201  oemapvali  9666  cantnflem1  9671  harval2  10005  zsupss  12989  ramub1lem1  17122  symggen  19598  efgsfo  19867  ablfacrp  20196  ablfac1eu  20203  pgpfac1lem5  20209  ablfaclem3  20217  nrmr0reg  23976  ptcmplem3  24281  abelthlem2  26665  lgamgulmlem1  27263  ltonold  28524  onsfi  28619  rspectopn  34364  fineqvnttrclselem1  35634  neibastop2lem  36966  topmeet  36970  weiunse  37074  cntotbnd  38533  mapdrvallem2  42505  aks6d1c6lem3  43025  onintunirab  44055  nadd2rabex  44214  k0004ss1  44978  liminfvalxr  46598