Metamath Proof Explorer


Theorem cp

Description: Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick scottex that collapses a proper class into a set of minimum rank. The wff ph can be thought of as ph ( x , y ) . Scheme "Collection Principle" of Jech p. 72. (Contributed by NM, 17-Oct-2003)

Ref Expression
Assertion cp wxzyφywφ

Proof

Step Hyp Ref Expression
1 vex zV
2 1 cplem2 wxzy|φy|φw
3 abn0 y|φyφ
4 elin yy|φwyy|φyw
5 abid yy|φφ
6 5 anbi1i yy|φywφyw
7 ancom φywywφ
8 4 6 7 3bitri yy|φwywφ
9 8 exbii yyy|φwyywφ
10 nfab1 _yy|φ
11 nfcv _yw
12 10 11 nfin _yy|φw
13 12 n0f y|φwyyy|φw
14 df-rex ywφyywφ
15 9 13 14 3bitr4i y|φwywφ
16 3 15 imbi12i y|φy|φwyφywφ
17 16 ralbii xzy|φy|φwxzyφywφ
18 17 exbii wxzy|φy|φwwxzyφywφ
19 2 18 mpbi wxzyφywφ