Metamath Proof Explorer

Theorem inecmo

Description: Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018)

		Ref	Expression
	Hypothesis	inecmo.1	$⊢ x = y \to B = C$
	Assertion	inecmo	$⊢ Rel R \to (\forall x \in A \forall y \in A (x = y \lor [B] R \cap [C] R = \emptyset) \leftrightarrow \forall z \exists^{*} x \in A B R z)$

Proof

Step	Hyp	Ref	Expression
1		inecmo.1	$⊢ x = y \to B = C$
2		ineleq	$⊢ \forall x \in A \forall y \in A (x = y \lor [B] R \cap [C] R = \emptyset) \leftrightarrow \forall x \in A \forall z \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y)$
3		ralcom4	$⊢ \forall x \in A \forall z \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y) \leftrightarrow \forall z \forall x \in A \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y)$
4	2 3	bitri	$⊢ \forall x \in A \forall y \in A (x = y \lor [B] R \cap [C] R = \emptyset) \leftrightarrow \forall z \forall x \in A \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y)$
5	1	breq1d	$⊢ x = y \to (B R z \leftrightarrow C R z)$
6	5	rmo4	$⊢ \exists^{*} x \in A B R z \leftrightarrow \forall x \in A \forall y \in A ((B R z \land C R z) \to x = y)$
7		relelec	$⊢ Rel R \to (z \in [B] R \leftrightarrow B R z)$
8		relelec	$⊢ Rel R \to (z \in [C] R \leftrightarrow C R z)$
9	7 8	anbi12d	$⊢ Rel R \to ((z \in [B] R \land z \in [C] R) \leftrightarrow (B R z \land C R z))$
10	9	imbi1d	$⊢ Rel R \to (((z \in [B] R \land z \in [C] R) \to x = y) \leftrightarrow ((B R z \land C R z) \to x = y))$
11	10	2ralbidv	$⊢ Rel R \to (\forall x \in A \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y) \leftrightarrow \forall x \in A \forall y \in A ((B R z \land C R z) \to x = y))$
12	6 11	bitr4id	$⊢ Rel R \to (\exists^{*} x \in A B R z \leftrightarrow \forall x \in A \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y))$
13	12	albidv	$⊢ Rel R \to (\forall z \exists^{*} x \in A B R z \leftrightarrow \forall z \forall x \in A \forall y \in A ((z \in [B] R \land z \in [C] R) \to x = y))$
14	4 13	bitr4id	$⊢ Rel R \to (\forall x \in A \forall y \in A (x = y \lor [B] R \cap [C] R = \emptyset) \leftrightarrow \forall z \exists^{*} x \in A B R z)$