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 
|- ( ( A = B /\ A e. C ) <-> ( A = B /\ B e. C ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( B = A /\ A e. C ) -> B = A )
2 eqeltr 
 |-  ( ( B = A /\ A e. C ) -> B e. C )
3 1 2 jca 
 |-  ( ( B = A /\ A e. C ) -> ( B = A /\ B e. C ) )
4 eqcom 
 |-  ( B = A <-> A = B )
5 4 anbi1i 
 |-  ( ( B = A /\ A e. C ) <-> ( A = B /\ A e. C ) )
6 4 anbi1i 
 |-  ( ( B = A /\ B e. C ) <-> ( A = B /\ B e. C ) )
7 3 5 6 3imtr3i 
 |-  ( ( A = B /\ A e. C ) -> ( A = B /\ B e. C ) )
8 simpl 
 |-  ( ( A = B /\ B e. C ) -> A = B )
9 eqeltr 
 |-  ( ( A = B /\ B e. C ) -> A e. C )
10 8 9 jca 
 |-  ( ( A = B /\ B e. C ) -> ( A = B /\ A e. C ) )
11 7 10 impbii 
 |-  ( ( A = B /\ A e. C ) <-> ( A = B /\ B e. C ) )