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

Metamath Proof Explorer

Theorem rabbi

Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii . (Contributed by NM, 25-Nov-2013)

Ref Expression
Assertion rabbi ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝜒 ) ↔ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐴 ∣ 𝜒 } )

Proof

Step Hyp Ref Expression
1 abbib ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
2 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
3 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) }
4 2 3 eqeq12i ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐴 ∣ 𝜒 } ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } )
5 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝜒 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
6 pm5.32 ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
7 6 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
8 5 7 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝜒 ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
9 1 4 8 3bitr4ri ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 ↔ 𝜒 ) ↔ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐴 ∣ 𝜒 } )