This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted existential uniqueness and at-most-one quantifier reuanid
Description: Cancellation law for restricted unique existential quantification.
(Contributed by Peter Mazsa , 12-Feb-2018) (Proof shortened by Wolf
Lammen , 12-Jan-2025)
Ref
Expression
Assertion
reuanid ⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑥 ∈ 𝐴 𝜑 )
Proof
Step
Hyp
Ref
Expression
1
ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
2
1
bicomd ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝜑 ) )
3
2
reubiia ⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑥 ∈ 𝐴 𝜑 )