Theorem prid2g 4123

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

Syntax hints:   -> wi 4   e. wcel 1823   {cpr 4018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-sn 4017  df-pr 4019

This theorem is referenced by:  unisn2  4573  fr2nr  4846  pw2f1olem  7614  hashprdifel  12447  gcdcllem3  14235  mgm2nsgrplem1  16235  mgm2nsgrplem2  16236  mgm2nsgrplem3  16237  sgrp2nmndlem1  16240  sgrp2rid2  16243  pmtrprfv  16677  m2detleib  19300  indistopon  19669  pptbas  19676  coseq0negpitopi  23062  usgra2edg  24584  nb3graprlem1  24653  nb3graprlem2  24654  2trllemF  24753  vdgr1b  25106  prsiga  28361  ftc1anclem8  30337  fourierdlem54  32182  imarnf1pr  32683  usgvad2edg  32783