Theorem prid2g 3981

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)

Assertion

Ref	Expression
prid2g	|- ( B e. V -> B e. { A , B } )

Proof of Theorem prid2g

Step	Hyp	Ref	Expression
1		prid1g 3980	. 2 |- ( B e. V -> B e. { B , A } )
2		prcom 3952	. 2 |- { B , A } = { A , B }
3	1, 2	syl6eleq 2532	1 |- ( B e. V -> B e. { A , B } )

Syntax hints:   -> wi 4   e. wcel 1756   {cpr 3878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2973  df-un 3332  df-sn 3877  df-pr 3879

This theorem is referenced by:  unisn2  4427  fr2nr  4697  pw2f1olem  7414  gcdcllem3  13696  pmtrprfv  15958  m2detleib  18436  indistopon  18604  pptbas  18611  coseq0negpitopi  21964  usgra2edg  23300  nb3graprlem1  23358  nb3graprlem2  23359  2trllemF  23447  vdgr1b  23573  prsiga  26573  ftc1anclem8  28472  imarnf1pr  30148