Theorem 2reu4

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

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

Proof

Step	Hyp	Ref	Expression
1		reurex	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
2		rexn0	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → 𝐴 ≠ ∅ )
3	1 2	syl	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → 𝐴 ≠ ∅ )
4		reurex	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
5		rexn0	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐵 ≠ ∅ )
6	4 5	syl	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐵 ≠ ∅ )
7	3 6	anim12i	⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
8		ne0i	⊢ ( 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
9		ne0i	⊢ ( 𝑦 ∈ 𝐵 → 𝐵 ≠ ∅ )
10	8 9	anim12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
11	10	a1d	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝜑 → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )
12	11	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
13	12	adantr	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
14		2reu4lem	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
15	7 13 14	pm5.21nii	⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )