Theorem prid2g 4122

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

Syntax hints:   -> wi 4   e. wcel 1804   {cpr 4016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017

This theorem is referenced by:  unisn2  4573  fr2nr  4847  pw2f1olem  7623  hashprdifel  12442  gcdcllem3  14028  mgm2nsgrplem1  15910  mgm2nsgrplem2  15911  mgm2nsgrplem3  15912  sgrp2nmndlem1  15915  sgrp2rid2  15918  pmtrprfv  16352  m2detleib  19006  indistopon  19375  pptbas  19382  coseq0negpitopi  22768  usgra2edg  24254  nb3graprlem1  24323  nb3graprlem2  24324  2trllemF  24423  vdgr1b  24776  prsiga  28004  ftc1anclem8  30072  fourierdlem54  31832  imarnf1pr  32147  usgvad2edg  32249