Metamath Proof Explorer

Theorem bnj1113

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

Ref Expression
Hypothesis bnj1113.1 
|- ( A = B -> C = D )
Assertion bnj1113 
|- ( A = B -> U_ x e. C E = U_ x e. D E )

Proof

Step Hyp Ref Expression
1 bnj1113.1 
 |-  ( A = B -> C = D )
2 1 iuneq1d 
 |-  ( A = B -> U_ x e. C E = U_ x e. D E )