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
Unicode
Syntax definition
w2reu
Description:
Syntax for double restricted existential uniqueness quantification.
Ref
Expression
Assertion
w2reu
wff
∃!
x
∈
A
,
y
∈
B
φ