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 2859	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  {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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  opi2  5438  opeluu  5439  opthwiener  5487  dmrnssfld  5956  funopg  6574  fprb  7199  1oelpr  8487  2dom  9058  dfac2b  10209  brdom7disj  10610  brdom6disj  10611  cnelprrecn  11293  1elpr01  11304  mnfxr  11366  seqexw  14160  m1expcl2  14228  hash2prb  14617  pr2pwpr  14624  cat1  18272  grpss  19165  dmdprdpr  20265  cnmsgnsubg  21883  m2detleiblem6  22941  m2detleiblem3  22944  m2detleiblem4  22945  m2detleib  22946  indiscld  23409  ehl2eudis  25743  aannenlem2  26656  taylthlem2  26701  ppiublem2  27530  lgsdir2lem3  27654  ltsres  28019  noextendgt  28027  nolesgn2ores  28029  nosepnelem  28036  nosepdmlem  28040  nolt02o  28052  nosupno  28060  nosupbnd1lem3  28067  nosupbnd1  28071  nosupbnd2lem1  28072  noetainflem1  28094  ecgrtg  29561  elntg  29562  wlk2v2e  30758  eulerpathpr  30841  ex-br  31032  ex-eprel  31034  trsp2cyc  33684  subfacp1lem3  35947  kur14lem7  35977  ex-sategoelel12  36192  onpsstopbas  37218  onint1  37237  bj-inftyexpidisj  38131  kelac2  44066  onnoxp  44433  clsk1indlem1  45044  mnuprdlem2  45256  mnuprdlem3  45257  mnurndlem1  45264  refsum2cnlem1  46053  fourierdlem103  47218  fourierdlem104  47219  ioorrnopn  47314  ioorrnopnxr  47316  grlimgrtrilem1  49098  pglem  49188  zlmodzxzldeplem3  49613  nn0sumshdiglemB  49731  rrx2pyel  49823  rrx2linesl  49854  2sphere0  49861  termc2  50625