Theorem prid2g 4140

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 4139	. 2 |- ( B e. V -> B e. { B , A } )
2		prcom 4111	. 2 |- { B , A } = { A , B }
3	1, 2	syl6eleq 2565	1 |- ( B e. V -> B e. { A , B } )

Syntax hints:   -> wi 4   e. wcel 1767   {cpr 4035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-un 3486  df-sn 4034  df-pr 4036

This theorem is referenced by:  unisn2  4589  fr2nr  4863  pw2f1olem  7633  hashprdifel  12443  gcdcllem3  14027  mgm2nsgrplem1  15908  mgm2nsgrplem2  15909  mgm2nsgrplem3  15910  sgrp2nmndlem1  15913  sgrp2rid2  15916  pmtrprfv  16351  m2detleib  19002  indistopon  19370  pptbas  19377  coseq0negpitopi  22762  usgra2edg  24205  nb3graprlem1  24274  nb3graprlem2  24275  2trllemF  24374  vdgr1b  24727  prsiga  27956  ftc1anclem8  30024  fourierdlem54  31784  imarnf1pr  32099  usgvad2edg  32201