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 → B = C
Assertion inecmo ⊢ Rel ⁡ R → ∀ x ∈ A ∀ y ∈ A x = y ∨ B R ∩ C R = ∅ ↔ ∀ z ∃* x ∈ A B R z

Proof

Step Hyp Ref Expression
1 inecmo.1 ⊢ x = y → B = C
2 ineleq ⊢ ∀ x ∈ A ∀ y ∈ A x = y ∨ B R ∩ C R = ∅ ↔ ∀ x ∈ A ∀ z ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y
3 ralcom4 ⊢ ∀ x ∈ A ∀ z ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y ↔ ∀ z ∀ x ∈ A ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y
4 2 3 bitri ⊢ ∀ x ∈ A ∀ y ∈ A x = y ∨ B R ∩ C R = ∅ ↔ ∀ z ∀ x ∈ A ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y
5 1 breq1d ⊢ x = y → B R z ↔ C R z
6 5 rmo4 ⊢ ∃* x ∈ A B R z ↔ ∀ x ∈ A ∀ y ∈ A B R z ∧ C R z → x = y
7 relelec ⊢ Rel ⁡ R → z ∈ B R ↔ B R z
8 relelec ⊢ Rel ⁡ R → z ∈ C R ↔ C R z
9 7 8 anbi12d ⊢ Rel ⁡ R → z ∈ B R ∧ z ∈ C R ↔ B R z ∧ C R z
10 9 imbi1d ⊢ Rel ⁡ R → z ∈ B R ∧ z ∈ C R → x = y ↔ B R z ∧ C R z → x = y
11 10 2ralbidv ⊢ Rel ⁡ R → ∀ x ∈ A ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y ↔ ∀ x ∈ A ∀ y ∈ A B R z ∧ C R z → x = y
12 6 11 bitr4id ⊢ Rel ⁡ R → ∃* x ∈ A B R z ↔ ∀ x ∈ A ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y
13 12 albidv ⊢ Rel ⁡ R → ∀ z ∃* x ∈ A B R z ↔ ∀ z ∀ x ∈ A ∀ y ∈ A z ∈ B R ∧ z ∈ C R → x = y
14 4 13 bitr4id ⊢ Rel ⁡ R → ∀ x ∈ A ∀ y ∈ A x = y ∨ B R ∩ C R = ∅ ↔ ∀ z ∃* x ∈ A B R z