Theorem prid2 3711

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
prid2.1	|- B e. _V

Assertion

Ref	Expression
prid2	|- B e. { A , B }

Proof of Theorem prid2

Step	Hyp	Ref	Expression
1		prid2.1	. . 3 |- B e. _V
2	1	prid1 3710	. 2 |- B e. { B , A }
3		prcom 3680	. 2 |- { B , A } = { A , B }
4	2, 3	eleqtri 2262	1 |- B e. { A , B }

Syntax hints:   e. wcel 2158   _Vcvv 2749   {cpr 3605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611

This theorem is referenced by:  prel12  3783  opi2  4245  opeluu  4462  ontr2exmid  4536  onsucelsucexmid  4541  regexmidlemm  4543  ordtri2or2exmid  4582  ontri2orexmidim  4583  dmrnssfld  4902  funopg  5262  acexmidlema  5879  acexmidlemcase  5883  acexmidlem2  5885  1lt2o  6457  2dom  6819  unfiexmid  6931  djuss  7083  exmidonfinlem  7206  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  exmidaclem  7221  cnelprrecn  7961  mnfxr  8028  sup3exmid  8928  m1expcl2  10556  fnpr2ob  12778  lgsdir2lem3  14784  bdop  14980  2o01f  15100  iswomni0  15153