Theorem ss2rabdv 4099

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 3152	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
3		ss2rab 4094	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4	2, 3	sylibr 234	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067  {crab 3443   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rab 3444  df-ss 3993

This theorem is referenced by:  rabssrabd  4106  sess1  5665  suppssov1  8238  suppssov2  8239  suppssfv  8243  cofon1  8728  naddssim  8741  harword  9632  scottex  9954  mrcss  17674  ablfac1b  20114  mptscmfsupp0  20947  lspss  21005  dsmmacl  21784  dsmmsubg  21786  dsmmlss  21787  aspss  21920  psdmul  22193  scmatdmat  22542  clsss  23083  lfinpfin  23553  qustgpopn  24149  metss2lem  24545  equivcau  25353  rrxmvallem  25457  ovolsslem  25538  itg2monolem1  25805  lgamucov  27099  sqff1o  27243  musum  27252  madess  27933  cofcut1  27972  cusgrfilem1  29491  clwlknf1oclwwlknlem3  30115  occon  31319  spanss  31380  rmfsupp2  33218  fldgenss  33283  locfinreflem  33786  omsmon  34263  orvclteinc  34440  fin2solem  37566  poimirlem26  37606  poimirlem27  37607  cnambfre  37628  pclssN  39851  2polssN  39872  dihglblem3N  41252  dochss  41322  mapdordlem2  41594  nna4b4nsq  42615  itgoss  43120  nzss  44286  ovnsslelem  46481  rmsuppss  48095  mndpsuppss  48096  scmsuppss  48097