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

Metamath Proof Explorer

Theorem op2nda

Description: Extract the second member of an ordered pair. (See op1sta to extract the first member, op2ndb for an alternate version, and op2nd for the preferred version.) (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypotheses cnvsn.1 ⊢ A ∈ V
cnvsn.2 ⊢ B ∈ V
Assertion op2nda ⊢ ⋃ ran ⁡ A B = B

Proof

Step Hyp Ref Expression
1 cnvsn.1 ⊢ A ∈ V
2 cnvsn.2 ⊢ B ∈ V
3 1 rnsnop ⊢ ran ⁡ A B = B
4 3 unieqi ⊢ ⋃ ran ⁡ A B = ⋃ B
5 2 unisn ⊢ ⋃ B = B
6 4 5 eqtri ⊢ ⋃ ran ⁡ A B = B