This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )