Theorem ss2rabi 3817

Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)

Hypothesis

Ref	Expression
ss2rabi.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
ss2rabi	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem ss2rabi

Step	Hyp	Ref	Expression
1		ss2rab 3811	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
2		ss2rabi.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	mprgbir 3057	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ∈ wcel 2131  {crab 3046   ⊆ wss 3707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rab 3051  df-in 3714  df-ss 3721

This theorem is referenced by:  supub  8522  suplub  8523  card2on  8616  rankval4  8895  fin1a2lem12  9417  catlid  16537  catrid  16538  gsumval2  17473  lbsextlem3  19354  psrbagsn  19689  musum  25108  ppiub  25120  umgrupgr  26189  umgrislfupgr  26209  usgruspgr  26264  usgrislfuspgr  26270  disjxwwlksn  27014  clwwlknclwwlkdifnum  27093  clwwlknclwwlkdifnumOLD  27095  konigsbergssiedgw  27394  dlwwlknonclwlknonf1olem2  27517  omssubadd  30663  bj-unrab  33220  poimirlem26  33740  poimirlem27  33741  lclkrs2  37323