Theorem ss2rabdv 4042

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045  {crab 3408   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rab 3409  df-ss 3934

This theorem is referenced by:  rabssrabd  4049  sess1  5606  suppssov1  8179  suppssov2  8180  suppssfv  8184  cofon1  8639  naddssim  8652  harword  9523  scottex  9845  mrcss  17584  mndpsuppss  18699  ablfac1b  20009  mptscmfsupp0  20840  lspss  20897  dsmmacl  21657  dsmmsubg  21659  dsmmlss  21660  aspss  21793  psdmul  22060  scmatdmat  22409  clsss  22948  lfinpfin  23418  qustgpopn  24014  metss2lem  24406  equivcau  25207  rrxmvallem  25311  ovolsslem  25392  itg2monolem1  25658  lgamucov  26955  sqff1o  27099  musum  27108  madess  27795  cofcut1  27835  bdayon  28180  cusgrfilem1  29390  clwlknf1oclwwlknlem3  30019  occon  31223  spanss  31284  rmfsupp2  33196  fldgenss  33273  locfinreflem  33837  omsmon  34296  orvclteinc  34474  fin2solem  37607  poimirlem26  37647  poimirlem27  37648  cnambfre  37669  pclssN  39895  2polssN  39916  dihglblem3N  41296  dochss  41366  mapdordlem2  41638  nna4b4nsq  42655  itgoss  43159  nzss  44313  ovnsslelem  46565  gpgusgralem  48051  rmsuppss  48362  scmsuppss  48363