Theorem ss2rabdv 3832

Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)

Hypothesis

Ref	Expression
ss2rabdv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ss2rabdv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem ss2rabdv

Step	Hyp	Ref	Expression
1		ss2rabdv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ralrimiva 3115	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
3		ss2rab 3827	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4	2, 3	sylibr 224	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2145  ∀wral 3061  {crab 3065   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-in 3730  df-ss 3737

This theorem is referenced by:  rabssrabd  3838  sess1  5218  suppfnssOLD  7475  suppssov1  7482  suppssfv  7486  harword  8629  mrcss  16483  ablfac1b  18676  mptscmfsupp0  19137  lspss  19196  aspss  19546  dsmmacl  20301  dsmmsubg  20303  dsmmlss  20304  scmatdmat  20538  clsss  21078  lfinpfin  21547  qustgpopn  22142  metss2lem  22535  equivcau  23316  rrxmvallem  23405  ovolsslem  23471  itg2monolem1  23736  lgamucov  24984  sqff1o  25128  musum  25137  cusgrfilem1  26585  clwlknf1oclwwlknlem3  27253  locfinreflem  30246  omsmon  30699  orvclteinc  30876  fin2solem  33727  poimirlem26  33767  poimirlem27  33768  cnambfre  33789  pclssN  35702  2polssN  35723  dihglblem3N  37105  dochss  37175  mapdordlem2  37447  nzss  39042  rmsuppss  42676  mndpsuppss  42677  scmsuppss  42678