Theorem ss2rabdv 4051

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051  {crab 3415   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rab 3416  df-ss 3943

This theorem is referenced by:  rabssrabd  4058  sess1  5619  suppssov1  8196  suppssov2  8197  suppssfv  8201  cofon1  8684  naddssim  8697  harword  9577  scottex  9899  mrcss  17628  mndpsuppss  18743  ablfac1b  20053  mptscmfsupp0  20884  lspss  20941  dsmmacl  21701  dsmmsubg  21703  dsmmlss  21704  aspss  21837  psdmul  22104  scmatdmat  22453  clsss  22992  lfinpfin  23462  qustgpopn  24058  metss2lem  24450  equivcau  25252  rrxmvallem  25356  ovolsslem  25437  itg2monolem1  25703  lgamucov  27000  sqff1o  27144  musum  27153  madess  27840  cofcut1  27880  bdayon  28225  cusgrfilem1  29435  clwlknf1oclwwlknlem3  30064  occon  31268  spanss  31329  rmfsupp2  33233  fldgenss  33310  locfinreflem  33871  omsmon  34330  orvclteinc  34508  fin2solem  37630  poimirlem26  37670  poimirlem27  37671  cnambfre  37692  pclssN  39913  2polssN  39934  dihglblem3N  41314  dochss  41384  mapdordlem2  41656  nna4b4nsq  42683  itgoss  43187  nzss  44341  ovnsslelem  46589  gpgusgralem  48060  rmsuppss  48345  scmsuppss  48346