This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The union of a class unipr
Description: The union of a pair is the union of its members. Proposition 5.7 of
TakeutiZaring p. 16. (Contributed by NM , 23-Aug-1993) (Proof
shortened by BJ , 1-Sep-2024)
Ref
Expression
Hypotheses
unipr.1 ⊢ 𝐴 ∈ V
unipr.2 ⊢ 𝐵 ∈ V
Assertion
unipr ⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
unipr.1 ⊢ 𝐴 ∈ V
2
unipr.2 ⊢ 𝐵 ∈ V
3
uniprg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
4
1 2 3
mp2an ⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 )