Metamath Proof Explorer

Theorem fnsnfvOLD

Description: Obsolete version of fnsnfv as of 8-Aug-2024. (Contributed by NM, 22-May-1998) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	fnsnfvOLD	$⊢ (F Fn A \land B \in A) \to \{F (B)\} = F [\{B\}]$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$⊢ y = F (B) \leftrightarrow F (B) = y$
2		fnbrfvb	$⊢ (F Fn A \land B \in A) \to (F (B) = y \leftrightarrow B F y)$
3	1 2	bitrid	$⊢ (F Fn A \land B \in A) \to (y = F (B) \leftrightarrow B F y)$
4	3	abbidv	$⊢ (F Fn A \land B \in A) \to \{y \| y = F (B)\} = \{y \| B F y\}$
5		df-sn	$⊢ \{F (B)\} = \{y \| y = F (B)\}$
6	5	a1i	$⊢ (F Fn A \land B \in A) \to \{F (B)\} = \{y \| y = F (B)\}$
7		fnrel	$⊢ F Fn A \to Rel F$
8		relimasn	$⊢ Rel F \to F [\{B\}] = \{y \| B F y\}$
9	7 8	syl	$⊢ F Fn A \to F [\{B\}] = \{y \| B F y\}$
10	9	adantr	$⊢ (F Fn A \land B \in A) \to F [\{B\}] = \{y \| B F y\}$
11	4 6 10	3eqtr4d	$⊢ (F Fn A \land B \in A) \to \{F (B)\} = F [\{B\}]$