Theorem cplem2

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

	Ref	Expression
Hypothesis	cplem2.1	|- A e. _V
Assertion	cplem2	|- E. y A. x e. A ( B =/= (/) -> ( B i^i y ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		cplem2.1	|- A e. _V
2		scottex	|- Scott B e. _V
3	1 2	iunex	|- U_ x e. A Scott B e. _V
4		nfiu1	|- F/_ x U_ x e. A Scott B
5	4	nfeq2	|- F/ x y = U_ x e. A Scott B
6		ineq2	|- ( y = U_ x e. A Scott B -> ( B i^i y ) = ( B i^i U_ x e. A Scott B ) )
7	6	neeq1d	|- ( y = U_ x e. A Scott B -> ( ( B i^i y ) =/= (/) <-> ( B i^i U_ x e. A Scott B ) =/= (/) ) )
8	7	imbi2d	|- ( y = U_ x e. A Scott B -> ( ( B =/= (/) -> ( B i^i y ) =/= (/) ) <-> ( B =/= (/) -> ( B i^i U_ x e. A Scott B ) =/= (/) ) ) )
9	5 8	ralbid	|- ( y = U_ x e. A Scott B -> ( A. x e. A ( B =/= (/) -> ( B i^i y ) =/= (/) ) <-> A. x e. A ( B =/= (/) -> ( B i^i U_ x e. A Scott B ) =/= (/) ) ) )
10		eqid	|- U_ x e. A Scott B = U_ x e. A Scott B
11	10	cplem1	|- A. x e. A ( B =/= (/) -> ( B i^i U_ x e. A Scott B ) =/= (/) )
12	3 9 11	ceqsexv2d	|- E. y A. x e. A ( B =/= (/) -> ( B i^i y ) =/= (/) )