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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3454  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  opi2  5442  opeluu  5443  opthwiener  5491  dmrnssfld  5961  funopg  6583  fprb  7209  1oelpr  8501  2dom  9072  dfac2b  10222  brdom7disj  10623  brdom6disj  10624  cnelprrecn  11306  1elpr01  11317  mnfxr  11379  seqexw  14173  m1expcl2  14241  hash2prb  14630  pr2pwpr  14637  cat1  18287  grpss  19180  dmdprdpr  20280  cnmsgnsubg  21898  m2detleiblem6  22956  m2detleiblem3  22959  m2detleiblem4  22960  m2detleib  22961  indiscld  23424  aannenlem2  26671  taylthlem2  26716  ppiublem2  27545  lgsdir2lem3  27669  ltsres  28034  noextendgt  28042  nolesgn2ores  28044  nosepnelem  28051  nosepdmlem  28055  nolt02o  28067  nosupno  28075  nosupbnd1lem3  28082  nosupbnd1  28086  nosupbnd2lem1  28087  noetainflem1  28109  ecgrtg  29576  elntg  29577  wlk2v2e  30773  eulerpathpr  30856  ex-br  31047  ex-eprel  31049  trsp2cyc  33740  subfacp1lem3  36071  kur14lem7  36101  ex-sategoelel12  36316  onpsstopbas  37348  onint1  37367  bj-inftyexpidisj  38274  kelac2  44210  onnoxp  44577  clsk1indlem1  45188  mnuprdlem2  45400  mnuprdlem3  45401  mnurndlem1  45408  refsum2cnlem1  46196  fourierdlem103  47361  fourierdlem104  47362  ioorrnopn  47457  ioorrnopnxr  47459  grlimgrtrilem1  49241  pglem  49331  zlmodzxzldeplem3  49756  nn0sumshdiglemB  49874  termc2  50795