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	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	bnj1542.2	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
	bnj1542.3	⊢ ( 𝜑 → 𝐹 ≠ 𝐺 )
	bnj1542.4	⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
Assertion	bnj1542	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1542.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		bnj1542.2	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
3		bnj1542.3	⊢ ( 𝜑 → 𝐹 ≠ 𝐺 )
4		bnj1542.4	⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
5		eqfnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
6	5	necon3abid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 ≠ 𝐺 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
7		df-ne	⊢ ( ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
8	7	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
9		rexnal	⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
10	8 9	bitri	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
11	6 10	bitr4di	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 ≠ 𝐺 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
12	1 2 11	syl2anc	⊢ ( 𝜑 → ( 𝐹 ≠ 𝐺 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
13	3 12	mpbid	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) )
14		nfv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 )
15	4	nfcii	⊢ Ⅎ 𝑥 𝐹
16		nfcv	⊢ Ⅎ 𝑥 𝑦
17	15 16	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
18		nfcv	⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑦 )
19	17 18	nfne	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 )
20		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
21		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
22	20 21	neeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
23	14 19 22	cbvrexw	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐺 ‘ 𝑦 ) )
24	13 23	sylibr	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) )