Metamath Proof Explorer


Theorem fiunlem

Description: Lemma for fiun and f1iun . Formerly part of f1iun . (Contributed by AV, 6-Oct-2023)

Ref Expression
Hypothesis fiun.1 x = y B = C
Assertion fiunlem B : D S y A B C C B u = B v z | x A z = B u v v u

Proof

Step Hyp Ref Expression
1 fiun.1 x = y B = C
2 vex v V
3 eqeq1 z = v z = B v = B
4 3 rexbidv z = v x A z = B x A v = B
5 2 4 elab v z | x A z = B x A v = B
6 1 eqeq2d x = y v = B v = C
7 6 cbvrexvw x A v = B y A v = C
8 r19.29 y A B C C B y A v = C y A B C C B v = C
9 sseq12 u = B v = C u v B C
10 9 ancoms v = C u = B u v B C
11 sseq12 v = C u = B v u C B
12 10 11 orbi12d v = C u = B u v v u B C C B
13 12 biimprcd B C C B v = C u = B u v v u
14 13 expdimp B C C B v = C u = B u v v u
15 14 rexlimivw y A B C C B v = C u = B u v v u
16 15 imp y A B C C B v = C u = B u v v u
17 8 16 sylan y A B C C B y A v = C u = B u v v u
18 17 an32s y A B C C B u = B y A v = C u v v u
19 18 adantlll B : D S y A B C C B u = B y A v = C u v v u
20 7 19 sylan2b B : D S y A B C C B u = B x A v = B u v v u
21 5 20 sylan2b B : D S y A B C C B u = B v z | x A z = B u v v u
22 21 ralrimiva B : D S y A B C C B u = B v z | x A z = B u v v u