Theorem prid2 4442

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

Syntax hints:   ∈ wcel 2139  Vcvv 3340  {cpr 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-sn 4322  df-pr 4324

This theorem is referenced by:  prel12OLD  4527  opi2  5086  opeluu  5087  opthwiener  5124  dmrnssfld  5539  funopg  6083  2dom  8194  dfac2b  9143  dfac2OLD  9145  brdom7disj  9545  brdom6disj  9546  cnelprrecn  10221  mnfxr  10288  m1expcl2  13076  hash2prb  13446  pr2pwpr  13453  sadcf  15377  xpsfrnel2  16427  setcepi  16939  grpss  17641  efgi1  18334  frgpuptinv  18384  dmdprdpr  18648  dprdpr  18649  cnmsgnsubg  20125  m2detleiblem6  20634  m2detleiblem3  20637  m2detleiblem4  20638  m2detleib  20639  indiscld  21097  xpstopnlem1  21814  xpstopnlem2  21816  i1f1lem  23655  i1f1  23656  aannenlem2  24283  taylthlem2  24327  ppiublem2  25127  lgsdir2lem3  25251  ecgrtg  26062  elntg  26063  usgr2trlncl  26866  umgrwwlks2on  27078  wlk2v2e  27309  eulerpathpr  27392  ex-br  27599  ex-eprel  27601  subfacp1lem3  31471  kur14lem7  31501  fprb  31976  sltres  32121  noextendgt  32129  nolesgn2ores  32131  nosepnelem  32136  nosepdmlem  32139  nolt02o  32151  nosupno  32155  nosupbnd1lem3  32162  nosupbnd1  32166  nosupbnd2lem1  32167  onpsstopbas  32735  onint1  32754  bj-inftyexpidisj  33408  kelac2  38137  fvrcllb1d  38489  relexp1idm  38508  corcltrcl  38533  cotrclrcl  38536  clsk1indlem1  38845  refsum2cnlem1  39695  limsup10exlem  40507  fourierdlem103  40929  fourierdlem104  40930  ioorrnopn  41028  ioorrnopnxr  41030  zlmodzxzscm  42645  zlmodzxzldeplem3  42801  nn0sumshdiglemB  42924