Metamath Proof Explorer

Theorem elunirn2OLD

Description: Obsolete version of elfvunirn as of 12-Jan-2025. (Contributed by Thierry Arnoux, 13-Nov-2016) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	elunirn2OLD	$⊢ (Fun F \land B \in F (A)) \to B \in ⋃ ran F$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ B \in F (A) \to A \in dom F$
2		fveq2	$⊢ x = A \to F (x) = F (A)$
3	2	eleq2d	$⊢ x = A \to (B \in F (x) \leftrightarrow B \in F (A))$
4	3	rspcev	$⊢ (A \in dom F \land B \in F (A)) \to \exists x \in dom F B \in F (x)$
5	1 4	mpancom	$⊢ B \in F (A) \to \exists x \in dom F B \in F (x)$
6	5	adantl	$⊢ (Fun F \land B \in F (A)) \to \exists x \in dom F B \in F (x)$
7		elunirn	$⊢ Fun F \to (B \in ⋃ ran F \leftrightarrow \exists x \in dom F B \in F (x))$
8	7	adantr	$⊢ (Fun F \land B \in F (A)) \to (B \in ⋃ ran F \leftrightarrow \exists x \in dom F B \in F (x))$
9	6 8	mpbird	$⊢ (Fun F \land B \in F (A)) \to B \in ⋃ ran F$