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 ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ { 𝑥 ∣ 𝜒 } )

Proof

Step Hyp Ref Expression
1 ss2abdv.1 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2 df-in ⊢ ( { 𝑥 ∣ 𝜓 } ∩ { 𝑥 ∣ 𝜒 } ) = { 𝑦 ∣ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) }
3 df-clab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
4 3 bicomi ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } )
5 df-clab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜒 } ↔ [ 𝑦 / 𝑥 ] 𝜒 )
6 5 bicomi ⊢ ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜒 } )
7 4 6 anbi12i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) )
8 7 abbii ⊢ { 𝑦 ∣ ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) } = { 𝑦 ∣ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) }
9 sbequ ⊢ ( 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑧 / 𝑥 ] 𝜓 ) )
10 sbequ ⊢ ( 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜒 ↔ [ 𝑧 / 𝑥 ] 𝜒 ) )
11 9 10 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜒 ) ) )
12 11 sbievw ⊢ ( [ 𝑧 / 𝑦 ] ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜒 ) )
13 ax-1 ⊢ ( [ 𝑧 / 𝑥 ] 𝜓 → ( [ 𝑧 / 𝑥 ] 𝜒 → [ 𝑧 / 𝑥 ] 𝜓 ) )
14 13 a1i ⊢ ( 𝜑 → ( [ 𝑧 / 𝑥 ] 𝜓 → ( [ 𝑧 / 𝑥 ] 𝜒 → [ 𝑧 / 𝑥 ] 𝜓 ) ) )
15 14 impd ⊢ ( 𝜑 → ( ( [ 𝑧 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜒 ) → [ 𝑧 / 𝑥 ] 𝜓 ) )
16 1 sbimdv ⊢ ( 𝜑 → ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜒 ) )
17 16 ancld ⊢ ( 𝜑 → ( [ 𝑧 / 𝑥 ] 𝜓 → ( [ 𝑧 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜒 ) ) )
18 15 17 impbid ⊢ ( 𝜑 → ( ( [ 𝑧 / 𝑥 ] 𝜓 ∧ [ 𝑧 / 𝑥 ] 𝜒 ) ↔ [ 𝑧 / 𝑥 ] 𝜓 ) )
19 12 18 bitrid ⊢ ( 𝜑 → ( [ 𝑧 / 𝑦 ] ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ [ 𝑧 / 𝑥 ] 𝜓 ) )
20 df-clab ⊢ ( 𝑧 ∈ { 𝑦 ∣ ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) } ↔ [ 𝑧 / 𝑦 ] ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) )
21 df-clab ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] 𝜓 )
22 19 20 21 3bitr4g ⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑦 ∣ ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) } ↔ 𝑧 ∈ { 𝑥 ∣ 𝜓 } ) )
23 22 eqrdv ⊢ ( 𝜑 → { 𝑦 ∣ ( [ 𝑦 / 𝑥 ] 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) } = { 𝑥 ∣ 𝜓 } )
24 8 23 eqtr3id ⊢ ( 𝜑 → { 𝑦 ∣ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) } = { 𝑥 ∣ 𝜓 } )
25 2 24 eqtrid ⊢ ( 𝜑 → ( { 𝑥 ∣ 𝜓 } ∩ { 𝑥 ∣ 𝜒 } ) = { 𝑥 ∣ 𝜓 } )
26 df-ss ⊢ ( { 𝑥 ∣ 𝜓 } ⊆ { 𝑥 ∣ 𝜒 } ↔ ( { 𝑥 ∣ 𝜓 } ∩ { 𝑥 ∣ 𝜒 } ) = { 𝑥 ∣ 𝜓 } )
27 25 26 sylibr ⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ { 𝑥 ∣ 𝜒 } )