Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006) Avoid axioms. (Revised by TM, 1-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ss2rabdv.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜒 ) ) | |
| Assertion | ss2rabdv | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜒 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ss2rabdv.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜒 ) ) | |
| 2 | 1 | imdistanda | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) ) |
| 3 | 2 | ss2abdv | ⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } ) |
| 4 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } | |
| 5 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } | |
| 6 | 3 4 5 | 3sstr4g | ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜒 } ) |