Theorem prid2 4724

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4722 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
prid2.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
prid2	⊢ 𝐵 ∈ {𝐴, 𝐵}

Proof of Theorem prid2

Step	Hyp	Ref	Expression
1		prid2.1	. . 3 ⊢ 𝐵 ∈ V
2	1	prid1 4723	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4693	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2858	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  {cpr 4586

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  opi2  5445  opeluu  5446  opthwiener  5491  dmrnssfld  5958  funopg  6568  fprb  7193  1oelpr  8469  2dom  9040  dfac2b  10136  brdom7disj  10537  brdom6disj  10538  cnelprrecn  11220  1elpr01  11231  mnfxr  11293  seqexw  14084  m1expcl2  14152  hash2prb  14540  pr2pwpr  14547  cat1  18189  grpss  19081  dmdprdpr  20181  cnmsgnsubg  21793  m2detleiblem6  22851  m2detleiblem3  22854  m2detleiblem4  22855  m2detleib  22856  indiscld  23319  ehl2eudis  25653  aannenlem2  26568  taylthlem2  26613  ppiublem2  27442  lgsdir2lem3  27566  ltsres  27901  noextendgt  27909  nolesgn2ores  27911  nosepnelem  27918  nosepdmlem  27922  nolt02o  27934  nosupno  27942  nosupbnd1lem3  27949  nosupbnd1  27953  nosupbnd2lem1  27954  noetainflem1  27976  ecgrtg  29443  elntg  29444  wlk2v2e  30640  eulerpathpr  30723  ex-br  30914  ex-eprel  30916  trsp2cyc  33566  subfacp1lem3  35764  kur14lem7  35794  ex-sategoelel12  36009  onpsstopbas  37052  onint1  37071  bj-inftyexpidisj  37965  kelac2  43909  onnoxp  44276  clsk1indlem1  44888  mnuprdlem2  45100  mnuprdlem3  45101  mnurndlem1  45108  refsum2cnlem1  45874  fourierdlem103  47040  fourierdlem104  47041  ioorrnopn  47136  ioorrnopnxr  47138  grlimgrtrilem1  48920  pglem  49010  zlmodzxzldeplem3  49435  nn0sumshdiglemB  49553  rrx2pyel  49645  rrx2linesl  49676  2sphere0  49683  termc2  50447