Theorem ss2rabdv 4039

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  {crab 3405   ⊆ wss 3914

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3406  df-ss 3931

This theorem is referenced by:  rabssrabd  4046  sess1  5603  suppssov1  8176  suppssov2  8177  suppssfv  8181  cofon1  8636  naddssim  8649  harword  9516  scottex  9838  mrcss  17577  mndpsuppss  18692  ablfac1b  20002  mptscmfsupp0  20833  lspss  20890  dsmmacl  21650  dsmmsubg  21652  dsmmlss  21653  aspss  21786  psdmul  22053  scmatdmat  22402  clsss  22941  lfinpfin  23411  qustgpopn  24007  metss2lem  24399  equivcau  25200  rrxmvallem  25304  ovolsslem  25385  itg2monolem1  25651  lgamucov  26948  sqff1o  27092  musum  27101  madess  27788  cofcut1  27828  bdayon  28173  cusgrfilem1  29383  clwlknf1oclwwlknlem3  30012  occon  31216  spanss  31277  rmfsupp2  33189  fldgenss  33266  locfinreflem  33830  omsmon  34289  orvclteinc  34467  fin2solem  37600  poimirlem26  37640  poimirlem27  37641  cnambfre  37662  pclssN  39888  2polssN  39909  dihglblem3N  41289  dochss  41359  mapdordlem2  41631  nna4b4nsq  42648  itgoss  43152  nzss  44306  ovnsslelem  46558  gpgusgralem  48047  rmsuppss  48358  scmsuppss  48359