Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Utility theorems
coexd
Next ⟩
elpwbi
Metamath Proof Explorer
Ascii
Unicode
Theorem
coexd
Description:
The composition of two sets is a set.
(Contributed by
SN
, 7-Feb-2025)
Ref
Expression
Hypotheses
coexd.1
⊢
φ
→
A
∈
V
coexd.2
⊢
φ
→
B
∈
W
Assertion
coexd
⊢
φ
→
A
∘
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
coexd.1
⊢
φ
→
A
∈
V
2
coexd.2
⊢
φ
→
B
∈
W
3
coexg
⊢
A
∈
V
∧
B
∈
W
→
A
∘
B
∈
V
4
1
2
3
syl2anc
⊢
φ
→
A
∘
B
∈
V