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 reueubd
Description: Restricted existential uniqueness is equivalent to existential
uniqueness if the unique element is in the restricting class.
(Contributed by AV , 4-Jan-2021)
Ref
Expression
Hypothesis
reueubd.1 ⊢ φ ∧ ψ → x ∈ V
Assertion
reueubd ⊢ φ → ∃! x ∈ V ψ ↔ ∃! x ψ
Proof
Step
Hyp
Ref
Expression
1
reueubd.1 ⊢ φ ∧ ψ → x ∈ V
2
df-reu ⊢ ∃! x ∈ V ψ ↔ ∃! x x ∈ V ∧ ψ
3
1
ex ⊢ φ → ψ → x ∈ V
4
3
pm4.71rd ⊢ φ → ψ ↔ x ∈ V ∧ ψ
5
4
eubidv ⊢ φ → ∃! x ψ ↔ ∃! x x ∈ V ∧ ψ
6
2 5
bitr4id ⊢ φ → ∃! x ∈ V ψ ↔ ∃! x ψ