Theorem prid2 4731

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.)

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 4730	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4700	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2863	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

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