Metamath Proof Explorer


Theorem cpcolld

Description: Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypotheses cpcolld.1 φ x A
cpcolld.2 φ x F y
Assertion cpcolld φ y F Coll A x F y

Proof

Step Hyp Ref Expression
1 cpcolld.1 φ x A
2 cpcolld.2 φ x F y
3 vex y V
4 breq2 z = y x F z x F y
5 3 4 elab y z | x F z x F y
6 2 5 sylibr φ y z | x F z
7 6 19.8ad φ y y z | x F z
8 7 scotteld φ y y Scott z | x F z
9 ssiun2 x A Scott z | x F z x A Scott z | x F z
10 dfcoll2 F Coll A = x A Scott z | x F z
11 9 10 sseqtrrdi x A Scott z | x F z F Coll A
12 11 sselda x A y Scott z | x F z y F Coll A
13 4 elscottab y Scott z | x F z x F y
14 13 adantl x A y Scott z | x F z x F y
15 12 14 jca x A y Scott z | x F z y F Coll A x F y
16 15 ex x A y Scott z | x F z y F Coll A x F y
17 16 eximdv x A y y Scott z | x F z y y F Coll A x F y
18 1 8 17 sylc φ y y F Coll A x F y
19 df-rex y F Coll A x F y y y F Coll A x F y
20 18 19 sylibr φ y F Coll A x F y