Metamath Proof Explorer

Theorem bnj1322

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1322 
|- ( A = B -> ( A i^i B ) = A )

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( A = B -> A C_ B )
2 dfss2 
 |-  ( A C_ B <-> ( A i^i B ) = A )
3 1 2 sylib 
 |-  ( A = B -> ( A i^i B ) = A )