2reu4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 2reu4		Structured version Visualization version GIF version

Theorem 2reu4 4484

Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2681. (Contributed by Alexander van der Vekens, 1-Jul-2017.)

**Assertion**
Ref	Expression
2reu4	⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))

Distinct variable groups: 𝑧,𝑤,𝜑 𝑥,𝑤,𝑦,𝐴,𝑧 𝑤,𝐵,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑥, 𝑦)

**Proof of Theorem 2reu4**
Step	Hyp	Ref	Expression
1		reurex 3372	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
2		rexn0 4456	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝐴 ≠ ∅)
3	1, 2	syl 18	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝐴 ≠ ∅)
4		reurex 3372	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
5		rexn0 4456	. . . 4 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → 𝐵 ≠ ∅)
6	4, 5	syl 18	. . 3 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 → 𝐵 ≠ ∅)
7	3, 6	anim12i 624	. 2 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
8		ne0i 4293	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
9		ne0i 4293	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 → 𝐵 ≠ ∅)
10	8, 9	anim12i 624	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
11	10	a1d 26	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅)))
12	11	rexlimivv 3206	. . 3 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
13	12	adantr 485	. 2 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
14		2reu4lem 4483	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
15	7, 13, 14	pm5.21nii 381	1 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ∃!wreu 3366 ∅c0 4285

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-dif 3907 df-nul 4286

This theorem is used by: opreu2reurex 6295 opreu2reuALT 32834

W3C validator