Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Replacement
Theorems requiring subset and intersection existence
difexd
Next ⟩
zfausab
Metamath Proof Explorer
Ascii
Unicode
Theorem
difexd
Description:
Existence of a difference.
(Contributed by
SN
, 16-Jul-2024)
Ref
Expression
Hypothesis
difexd.1
⊢
φ
→
A
∈
V
Assertion
difexd
⊢
φ
→
A
∖
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
difexd.1
⊢
φ
→
A
∈
V
2
difexg
⊢
A
∈
V
→
A
∖
B
∈
V
3
1
2
syl
⊢
φ
→
A
∖
B
∈
V