This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unisn3

Description: Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008)

Ref Expression
Assertion unisn3 ⊢ A ∈ B → ⋃ x ∈ B | x = A = A

Proof

Step Hyp Ref Expression
1 rabsn ⊢ A ∈ B → x ∈ B | x = A = A
2 1 unieqd ⊢ A ∈ B → ⋃ x ∈ B | x = A = ⋃ A
3 unisng ⊢ A ∈ B → ⋃ A = A
4 2 3 eqtrd ⊢ A ∈ B → ⋃ x ∈ B | x = A = A