![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > op2nda | Structured version Visualization version Unicode version |
Description: Extract the second member of an ordered pair. (See op1sta 5321 to extract the first member, op2ndb 5323 for an alternate version, and op2nd 6807 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
cnvsn.1 |
![]() ![]() ![]() ![]() |
cnvsn.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
op2nda |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvsn.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | rnsnop 5320 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | unieqi 4210 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | cnvsn.2 |
. . 3
![]() ![]() ![]() ![]() | |
5 | 4 | unisn 4216 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | eqtri 2475 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-xp 4843 df-rel 4844 df-cnv 4845 df-dm 4847 df-rn 4848 |
This theorem is referenced by: elxp4 6742 elxp5 6743 op2nd 6807 fo2nd 6819 f2ndres 6821 ixpsnf1o 7567 xpassen 7671 xpdom2 7672 |
Copyright terms: Public domain | W3C validator |