This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abbib

Description: Equal class abstractions require equivalent formulas, and conversely. (Contributed by NM, 25-Nov-2013) (Revised by Mario Carneiro, 11-Aug-2016) Remove dependency on ax-8 and df-clel (by avoiding use of cleqh ). (Revised by BJ, 23-Jun-2019) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025)

Ref Expression
Assertion abbib ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
2 nfsab1 ⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
3 nfsab1 ⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜓 }
4 2 3 nfbi ⊢ Ⅎ 𝑥 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } )
5 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ↔ 𝜓 )
6 df-clab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
7 sbequ12r ⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
8 6 7 bitrid ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) )
9 df-clab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
10 sbequ12r ⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜓 ) )
11 9 10 bitrid ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜓 ) )
12 8 11 bibi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
13 4 5 12 cbvalv1 ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )
14 1 13 bitri ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )