Theorem prid2 4734

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4732 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 4733	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4703	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2864	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  {cpr 4596

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 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  opi2  5456  opeluu  5457  opthwiener  5502  dmrnssfld  5969  funopg  6577  fprb  7199  1oelpr  8473  2dom  9037  dfac2b  10133  brdom7disj  10533  brdom6disj  10534  cnelprrecn  11211  1elpr01  11222  mnfxr  11284  seqexw  14073  m1expcl2  14141  hash2prb  14529  pr2pwpr  14536  cat1  18179  grpss  19046  dmdprdpr  20146  cnmsgnsubg  21757  m2detleiblem6  22813  m2detleiblem3  22816  m2detleiblem4  22817  m2detleib  22818  indiscld  23278  ehl2eudis  25611  aannenlem2  26522  taylthlem2  26567  ppiublem2  27397  lgsdir2lem3  27521  ltsres  27856  noextendgt  27864  nolesgn2ores  27866  nosepnelem  27873  nosepdmlem  27877  nolt02o  27889  nosupno  27897  nosupbnd1lem3  27904  nosupbnd1  27908  nosupbnd2lem1  27909  noetainflem1  27931  ecgrtg  29363  elntg  29364  wlk2v2e  30538  eulerpathpr  30621  ex-br  30812  ex-eprel  30814  trsp2cyc  33467  subfacp1lem3  35687  kur14lem7  35717  ex-sategoelel12  35932  onpsstopbas  36974  onint1  36993  bj-inftyexpidisj  37887  kelac2  43825  onnoxp  44192  clsk1indlem1  44804  mnuprdlem2  45016  mnuprdlem3  45017  mnurndlem1  45024  refsum2cnlem1  45790  fourierdlem103  46956  fourierdlem104  46957  ioorrnopn  47052  ioorrnopnxr  47054  grlimgrtrilem1  48799  pglem  48889  zlmodzxzldeplem3  49315  nn0sumshdiglemB  49433  rrx2pyel  49525  rrx2linesl  49556  2sphere0  49563  termc2  50329