Metamath Proof Explorer

Theorem supeq123d

Description: Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses supeq123d.a ⊢φ→A=D
supeq123d.b ⊢φ→B=E
supeq123d.c ⊢φ→C=F
Assertion supeq123d ⊢φ→supABC=supDEF

Proof

Step Hyp Ref Expression
1 supeq123d.a ⊢φ→A=D
2 supeq123d.b ⊢φ→B=E
3 supeq123d.c ⊢φ→C=F
4 3 breqd ⊢φ→xCy↔xFy
5 4 notbid ⊢φ→¬xCy↔¬xFy
6 1 5 raleqbidv ⊢φ→∀y∈A¬xCy↔∀y∈D¬xFy
7 3 breqd ⊢φ→yCx↔yFx
8 3 breqd ⊢φ→yCz↔yFz
9 1 8 rexeqbidv ⊢φ→∃z∈AyCz↔∃z∈DyFz
10 7 9 imbi12d ⊢φ→yCx→∃z∈AyCz↔yFx→∃z∈DyFz
11 2 10 raleqbidv ⊢φ→∀y∈ByCx→∃z∈AyCz↔∀y∈EyFx→∃z∈DyFz
12 6 11 anbi12d ⊢φ→∀y∈A¬xCy∧∀y∈ByCx→∃z∈AyCz↔∀y∈D¬xFy∧∀y∈EyFx→∃z∈DyFz
13 2 12 rabeqbidv ⊢φ→x∈B|∀y∈A¬xCy∧∀y∈ByCx→∃z∈AyCz=x∈E|∀y∈D¬xFy∧∀y∈EyFx→∃z∈DyFz
14 13 unieqd ⊢φ→⋃x∈B|∀y∈A¬xCy∧∀y∈ByCx→∃z∈AyCz=⋃x∈E|∀y∈D¬xFy∧∀y∈EyFx→∃z∈DyFz
15 df-sup ⊢supABC=⋃x∈B|∀y∈A¬xCy∧∀y∈ByCx→∃z∈AyCz
16 df-sup ⊢supDEF=⋃x∈E|∀y∈D¬xFy∧∀y∈EyFx→∃z∈DyFz
17 14 15 16 3eqtr4g ⊢φ→supABC=supDEF