Metamath Proof Explorer

Theorem ss2abdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) Avoid ax-8 , ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

Ref Expression
Hypothesis ss2abdv.1 ⊢ φ → ψ → χ
Assertion ss2abdv ⊢ φ → x | ψ ⊆ x | χ

Proof

Step Hyp Ref Expression
1 ss2abdv.1 ⊢ φ → ψ → χ
2 df-in ⊢ x | ψ ∩ x | χ = y | y ∈ x | ψ ∧ y ∈ x | χ
3 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
4 3 bicomi ⊢ y x ψ ↔ y ∈ x | ψ
5 df-clab ⊢ y ∈ x | χ ↔ y x χ
6 5 bicomi ⊢ y x χ ↔ y ∈ x | χ
7 4 6 anbi12i ⊢ y x ψ ∧ y x χ ↔ y ∈ x | ψ ∧ y ∈ x | χ
8 7 abbii ⊢ y | y x ψ ∧ y x χ = y | y ∈ x | ψ ∧ y ∈ x | χ
9 sbequ ⊢ y = z → y x ψ ↔ z x ψ
10 sbequ ⊢ y = z → y x χ ↔ z x χ
11 9 10 anbi12d ⊢ y = z → y x ψ ∧ y x χ ↔ z x ψ ∧ z x χ
12 11 sbievw ⊢ z y y x ψ ∧ y x χ ↔ z x ψ ∧ z x χ
13 ax-1 ⊢ z x ψ → z x χ → z x ψ
14 13 a1i ⊢ φ → z x ψ → z x χ → z x ψ
15 14 impd ⊢ φ → z x ψ ∧ z x χ → z x ψ
16 1 sbimdv ⊢ φ → z x ψ → z x χ
17 16 ancld ⊢ φ → z x ψ → z x ψ ∧ z x χ
18 15 17 impbid ⊢ φ → z x ψ ∧ z x χ ↔ z x ψ
19 12 18 bitrid ⊢ φ → z y y x ψ ∧ y x χ ↔ z x ψ
20 df-clab ⊢ z ∈ y | y x ψ ∧ y x χ ↔ z y y x ψ ∧ y x χ
21 df-clab ⊢ z ∈ x | ψ ↔ z x ψ
22 19 20 21 3bitr4g ⊢ φ → z ∈ y | y x ψ ∧ y x χ ↔ z ∈ x | ψ
23 22 eqrdv ⊢ φ → y | y x ψ ∧ y x χ = x | ψ
24 8 23 eqtr3id ⊢ φ → y | y ∈ x | ψ ∧ y ∈ x | χ = x | ψ
25 2 24 eqtrid ⊢ φ → x | ψ ∩ x | χ = x | ψ
26 df-ss ⊢ x | ψ ⊆ x | χ ↔ x | ψ ∩ x | χ = x | ψ
27 25 26 sylibr ⊢ φ → x | ψ ⊆ x | χ