Description: Obsolete version of unieq as of 13-Apr-2024. (Contributed by NM, 10-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.) 29-Jun-2011.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unieqOLD | |- ( A = B -> U. A = U. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexeq | |- ( A = B -> ( E. x e. A y e. x <-> E. x e. B y e. x ) ) |
|
| 2 | 1 | abbidv | |- ( A = B -> { y | E. x e. A y e. x } = { y | E. x e. B y e. x } ) |
| 3 | dfuni2 | |- U. A = { y | E. x e. A y e. x } |
|
| 4 | dfuni2 | |- U. B = { y | E. x e. B y e. x } |
|
| 5 | 2 3 4 | 3eqtr4g | |- ( A = B -> U. A = U. B ) |