Theorem 2reureurex 33078

Description: Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.)

Assertion

Ref	Expression
2reureurex	⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)

Proof of Theorem 2reureurex

Step	Hyp	Ref	Expression
1		df-2reu 33075	. 2 ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))
2	1	simplbi 502	1 ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4  ∃wrex 3086  ∃!wreu 3363  ∃!w2reu 33074

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-2reu 33075

This theorem is used by: (None)