Metamath Proof Explorer


Theorem unjust

Description: Soundness justification theorem for df-un . (Contributed by Rodolfo Medina, 28-Apr-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion unjust x | x A x B = y | y A y B

Proof

Step Hyp Ref Expression
1 eleq1w x = z x A z A
2 eleq1w x = z x B z B
3 1 2 orbi12d x = z x A x B z A z B
4 3 cbvabv x | x A x B = z | z A z B
5 eleq1w z = y z A y A
6 eleq1w z = y z B y B
7 5 6 orbi12d z = y z A z B y A y B
8 7 cbvabv z | z A z B = y | y A y B
9 4 8 eqtri x | x A x B = y | y A y B