| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > prid2 | Structured version Visualization version GIF version | ||
| Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4729 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.) |
| Ref | Expression |
|---|---|
| prid2.1 | ⊢ 𝐵 ∈ V |
| Ref | Expression |
|---|---|
| prid2 | ⊢ 𝐵 ∈ {𝐴, 𝐵} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prid2.1 | . . 3 ⊢ 𝐵 ∈ V | |
| 2 | 1 | prid1 4730 | . 2 ⊢ 𝐵 ∈ {𝐵, 𝐴} |
| 3 | prcom 4700 | . 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵} | |
| 4 | 2, 3 | eleqtri 2863 | 1 ⊢ 𝐵 ∈ {𝐴, 𝐵} |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ∈ wcel 2146 Vcvv 3457 {cpr 4593 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-v 3459 df-un 3911 df-sn 4592 df-pr 4594 |
| This theorem is used by: opi2 5453 opeluu 5454 opthwiener 5499 dmrnssfld 5966 funopg 6574 fprb 7198 1oelpr 8470 2dom 9034 dfac2b 10130 brdom7disj 10530 brdom6disj 10531 cnelprrecn 11210 1elpr01 11221 mnfxr 11283 seqexw 14073 m1expcl2 14141 hash2prb 14529 pr2pwpr 14536 cat1 18178 grpss 19067 dmdprdpr 20167 cnmsgnsubg 21779 m2detleiblem6 22835 m2detleiblem3 22838 m2detleiblem4 22839 m2detleib 22840 indiscld 23300 ehl2eudis 25634 aannenlem2 26545 taylthlem2 26590 ppiublem2 27420 lgsdir2lem3 27544 ltsres 27879 noextendgt 27887 nolesgn2ores 27889 nosepnelem 27896 nosepdmlem 27900 nolt02o 27912 nosupno 27920 nosupbnd1lem3 27927 nosupbnd1 27931 nosupbnd2lem1 27932 noetainflem1 27954 ecgrtg 29390 elntg 29391 wlk2v2e 30581 eulerpathpr 30664 ex-br 30855 ex-eprel 30857 trsp2cyc 33509 subfacp1lem3 35713 kur14lem7 35743 ex-sategoelel12 35958 onpsstopbas 37000 onint1 37019 bj-inftyexpidisj 37913 kelac2 43852 onnoxp 44219 clsk1indlem1 44831 mnuprdlem2 45043 mnuprdlem3 45044 mnurndlem1 45051 refsum2cnlem1 45817 fourierdlem103 46983 fourierdlem104 46984 ioorrnopn 47079 ioorrnopnxr 47081 grlimgrtrilem1 48826 pglem 48916 zlmodzxzldeplem3 49341 nn0sumshdiglemB 49459 rrx2pyel 49551 rrx2linesl 49582 2sphere0 49589 termc2 50355 |
| Copyright terms: Public domain | W3C validator |