bnj927

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

Step	Hyp	Ref	Expression
1		bnj927.1	$⊢ G = f \cup \{⟨n, C⟩\}$
2		bnj927.2	$⊢ C \in V$
3		simpr	$⊢ (p = suc n \land f Fn n) \to f Fn n$
4		vex	$⊢ n \in V$
5	4 2	fnsn	$⊢ \{⟨n, C⟩\} Fn \{n\}$
6	5	a1i	$⊢ (p = suc n \land f Fn n) \to \{⟨n, C⟩\} Fn \{n\}$
7		disjcsn	$⊢ n \cap \{n\} = \emptyset$
8	7	a1i	$⊢ (p = suc n \land f Fn n) \to n \cap \{n\} = \emptyset$
9	3 6 8	fnund	$⊢ (p = suc n \land f Fn n) \to (f \cup \{⟨n, C⟩\}) Fn (n \cup \{n\})$
10	1	fneq1i	$⊢ G Fn (n \cup \{n\}) \leftrightarrow (f \cup \{⟨n, C⟩\}) Fn (n \cup \{n\})$
11	9 10	sylibr	$⊢ (p = suc n \land f Fn n) \to G Fn (n \cup \{n\})$
12		df-suc	$⊢ suc n = n \cup \{n\}$
13	12	eqeq2i	$⊢ p = suc n \leftrightarrow p = n \cup \{n\}$
14	13	biimpi	$⊢ p = suc n \to p = n \cup \{n\}$
15	14	adantr	$⊢ (p = suc n \land f Fn n) \to p = n \cup \{n\}$
16	15	fneq2d	$⊢ (p = suc n \land f Fn n) \to (G Fn p \leftrightarrow G Fn (n \cup \{n\}))$
17	11 16	mpbird	$⊢ (p = suc n \land f Fn n) \to G Fn p$

Metamath Proof Explorer