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	|- E. w A. x e. z ( E. y ph -> E. y e. w ph )

Proof

Step	Hyp	Ref	Expression
1		vex	|- z e. _V
2	1	cplem2	|- E. w A. x e. z ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) )
3		abn0	|- ( { y | ph } =/= (/) <-> E. y ph )
4		elin	|- ( y e. ( { y | ph } i^i w ) <-> ( y e. { y | ph } /\ y e. w ) )
5		abid	|- ( y e. { y | ph } <-> ph )
6	5	anbi1i	|- ( ( y e. { y | ph } /\ y e. w ) <-> ( ph /\ y e. w ) )
7		ancom	|- ( ( ph /\ y e. w ) <-> ( y e. w /\ ph ) )
8	4 6 7	3bitri	|- ( y e. ( { y | ph } i^i w ) <-> ( y e. w /\ ph ) )
9	8	exbii	|- ( E. y y e. ( { y | ph } i^i w ) <-> E. y ( y e. w /\ ph ) )
10		nfab1	|- F/_ y { y | ph }
11		nfcv	|- F/_ y w
12	10 11	nfin	|- F/_ y ( { y | ph } i^i w )
13	12	n0f	|- ( ( { y | ph } i^i w ) =/= (/) <-> E. y y e. ( { y | ph } i^i w ) )
14		df-rex	|- ( E. y e. w ph <-> E. y ( y e. w /\ ph ) )
15	9 13 14	3bitr4i	|- ( ( { y | ph } i^i w ) =/= (/) <-> E. y e. w ph )
16	3 15	imbi12i	|- ( ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) ) <-> ( E. y ph -> E. y e. w ph ) )
17	16	ralbii	|- ( A. x e. z ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) ) <-> A. x e. z ( E. y ph -> E. y e. w ph ) )
18	17	exbii	|- ( E. w A. x e. z ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) ) <-> E. w A. x e. z ( E. y ph -> E. y e. w ph ) )
19	2 18	mpbi	|- E. w A. x e. z ( E. y ph -> E. y e. w ph )