Metamath Proof Explorer


Theorem iunssOLD

Description: Obsolete version of iunss as of 2-Feb-2026. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iunssOLD x A B C x A B C

Proof

Step Hyp Ref Expression
1 df-iun x A B = y | x A y B
2 1 sseq1i x A B C y | x A y B C
3 abss y | x A y B C y x A y B y C
4 df-ss B C y y B y C
5 4 ralbii x A B C x A y y B y C
6 ralcom4 x A y y B y C y x A y B y C
7 r19.23v x A y B y C x A y B y C
8 7 albii y x A y B y C y x A y B y C
9 5 6 8 3bitrri y x A y B y C x A B C
10 2 3 9 3bitri x A B C x A B C