exan3

Description: Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021)

		Ref	Expression
	Assertion	exan3	$⊢ (A \in V \land B \in W) \to (\exists u (A \in [u] R \land B \in [u] R) \leftrightarrow \exists u (u R A \land u R B))$

Step	Hyp	Ref	Expression
1		elecALTV	$⊢ (u \in V \land A \in V) \to (A \in [u] R \leftrightarrow u R A)$
2	1	el2v1	$⊢ A \in V \to (A \in [u] R \leftrightarrow u R A)$
3		elecALTV	$⊢ (u \in V \land B \in W) \to (B \in [u] R \leftrightarrow u R B)$
4	3	el2v1	$⊢ B \in W \to (B \in [u] R \leftrightarrow u R B)$
5	2 4	bi2anan9	$⊢ (A \in V \land B \in W) \to ((A \in [u] R \land B \in [u] R) \leftrightarrow (u R A \land u R B))$
6	5	exbidv	$⊢ (A \in V \land B \in W) \to (\exists u (A \in [u] R \land B \in [u] R) \leftrightarrow \exists u (u R A \land u R B))$

Metamath Proof Explorer