Metamath Proof Explorer
Description: Inference of restricted abstraction subclass from implication.
(Contributed by NM, 14Oct1999)


Ref 
Expression 

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

Assertion 
ss2rabi 
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

ss2rab 
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) 
3 
2 1

mprgbir 
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } 