bnj1542

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

Step	Hyp	Ref	Expression
1		bnj1542.1	$⊢ φ \to F Fn A$
2		bnj1542.2	$⊢ φ \to G Fn A$
3		bnj1542.3	$⊢ φ \to F \neq G$
4		bnj1542.4	$⊢ w \in F \to \forall x w \in F$
5		eqfnfv	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow \forall y \in A F (y) = G (y))$
6	5	necon3abid	$⊢ (F Fn A \land G Fn A) \to (F \neq G \leftrightarrow \neg \forall y \in A F (y) = G (y))$
7		df-ne	$⊢ F (y) \neq G (y) \leftrightarrow \neg F (y) = G (y)$
8	7	rexbii	$⊢ \exists y \in A F (y) \neq G (y) \leftrightarrow \exists y \in A \neg F (y) = G (y)$
9		rexnal	$⊢ \exists y \in A \neg F (y) = G (y) \leftrightarrow \neg \forall y \in A F (y) = G (y)$
10	8 9	bitri	$⊢ \exists y \in A F (y) \neq G (y) \leftrightarrow \neg \forall y \in A F (y) = G (y)$
11	6 10	bitr4di	$⊢ (F Fn A \land G Fn A) \to (F \neq G \leftrightarrow \exists y \in A F (y) \neq G (y))$
12	1 2 11	syl2anc	$⊢ φ \to (F \neq G \leftrightarrow \exists y \in A F (y) \neq G (y))$
13	3 12	mpbid	$⊢ φ \to \exists y \in A F (y) \neq G (y)$
14		nfv	$⊢ Ⅎ y F (x) \neq G (x)$
15	4	nfcii	$⊢ \underline{Ⅎ} x F$
16		nfcv	$⊢ \underline{Ⅎ} x y$
17	15 16	nffv	$⊢ \underline{Ⅎ} x F (y)$
18		nfcv	$⊢ \underline{Ⅎ} x G (y)$
19	17 18	nfne	$⊢ Ⅎ x F (y) \neq G (y)$
20		fveq2	$⊢ x = y \to F (x) = F (y)$
21		fveq2	$⊢ x = y \to G (x) = G (y)$
22	20 21	neeq12d	$⊢ x = y \to (F (x) \neq G (x) \leftrightarrow F (y) \neq G (y))$
23	14 19 22	cbvrexw	$⊢ \exists x \in A F (x) \neq G (x) \leftrightarrow \exists y \in A F (y) \neq G (y)$
24	13 23	sylibr	$⊢ φ \to \exists x \in A F (x) \neq G (x)$

Metamath Proof Explorer