Theorem bnj1542

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1542.1	|- ( ph -> F Fn A )
	bnj1542.2	|- ( ph -> G Fn A )
	bnj1542.3	|- ( ph -> F =/= G )
	bnj1542.4	|- ( w e. F -> A. x w e. F )
Assertion	bnj1542	|- ( ph -> E. x e. A ( F ` x ) =/= ( G ` x ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1542.1	|- ( ph -> F Fn A )
2		bnj1542.2	|- ( ph -> G Fn A )
3		bnj1542.3	|- ( ph -> F =/= G )
4		bnj1542.4	|- ( w e. F -> A. x w e. F )
5		eqfnfv	|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. y e. A ( F ` y ) = ( G ` y ) ) )
6	5	necon3abid	|- ( ( F Fn A /\ G Fn A ) -> ( F =/= G <-> -. A. y e. A ( F ` y ) = ( G ` y ) ) )
7		df-ne	|- ( ( F ` y ) =/= ( G ` y ) <-> -. ( F ` y ) = ( G ` y ) )
8	7	rexbii	|- ( E. y e. A ( F ` y ) =/= ( G ` y ) <-> E. y e. A -. ( F ` y ) = ( G ` y ) )
9		rexnal	|- ( E. y e. A -. ( F ` y ) = ( G ` y ) <-> -. A. y e. A ( F ` y ) = ( G ` y ) )
10	8 9	bitri	|- ( E. y e. A ( F ` y ) =/= ( G ` y ) <-> -. A. y e. A ( F ` y ) = ( G ` y ) )
11	6 10	bitr4di	|- ( ( F Fn A /\ G Fn A ) -> ( F =/= G <-> E. y e. A ( F ` y ) =/= ( G ` y ) ) )
12	1 2 11	syl2anc	|- ( ph -> ( F =/= G <-> E. y e. A ( F ` y ) =/= ( G ` y ) ) )
13	3 12	mpbid	|- ( ph -> E. y e. A ( F ` y ) =/= ( G ` y ) )
14		nfv	|- F/ y ( F ` x ) =/= ( G ` x )
15	4	nfcii	|- F/_ x F
16		nfcv	|- F/_ x y
17	15 16	nffv	|- F/_ x ( F ` y )
18		nfcv	|- F/_ x ( G ` y )
19	17 18	nfne	|- F/ x ( F ` y ) =/= ( G ` y )
20		fveq2	|- ( x = y -> ( F ` x ) = ( F ` y ) )
21		fveq2	|- ( x = y -> ( G ` x ) = ( G ` y ) )
22	20 21	neeq12d	|- ( x = y -> ( ( F ` x ) =/= ( G ` x ) <-> ( F ` y ) =/= ( G ` y ) ) )
23	14 19 22	cbvrexw	|- ( E. x e. A ( F ` x ) =/= ( G ` x ) <-> E. y e. A ( F ` y ) =/= ( G ` y ) )
24	13 23	sylibr	|- ( ph -> E. x e. A ( F ` x ) =/= ( G ` x ) )