Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Predicate Calculus
Double restricted existential uniqueness quantification syntax
w2reu
Next ⟩
df-2reu
Metamath Proof Explorer
Ascii
Structured
Syntax definition
w2reu
Description:
Syntax for double restricted existential uniqueness quantification.
Ref
Expression
Assertion
w2reu
wff
∃!
𝑥
∈
𝐴
,
𝑦
∈
𝐵
𝜑