Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Primitive equivalent of ax-groth
expanduniss
Next ⟩
ismnuprim
Metamath Proof Explorer
Ascii
Unicode
Theorem
expanduniss
Description:
Expand
U. A C_ B
to primitives.
(Contributed by
Rohan Ridenour
, 13-Aug-2023)
Ref
Expression
Assertion
expanduniss
⊢
⋃
A
⊆
B
↔
∀
x
x
∈
A
→
∀
y
y
∈
x
→
y
∈
B
Proof
Step
Hyp
Ref
Expression
1
unissb
⊢
⋃
A
⊆
B
↔
∀
x
∈
A
x
⊆
B
2
dfss2
⊢
x
⊆
B
↔
∀
y
y
∈
x
→
y
∈
B
3
2
expandral
⊢
∀
x
∈
A
x
⊆
B
↔
∀
x
x
∈
A
→
∀
y
y
∈
x
→
y
∈
B
4
1
3
bitri
⊢
⋃
A
⊆
B
↔
∀
x
x
∈
A
→
∀
y
y
∈
x
→
y
∈
B