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

Metamath Proof Explorer

Theorem eqelb

Description: Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 17-Jul-2019)

Ref Expression
Assertion eqelb ( ( 𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐴 ∈ 𝐶 ) → 𝐵 = 𝐴 )
2 eqeltr ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐴 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
3 1 2 jca ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐵 = 𝐴 ∧ 𝐵 ∈ 𝐶 ) )
4 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
5 4 anbi1i ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐴 ∈ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
6 4 anbi1i ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐵 ∈ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) )
7 3 5 6 3imtr3i ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) )
8 simpl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 = 𝐵 )
9 eqeltr ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 )
10 8 9 jca ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
11 7 10 impbii ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶 ) )