Theorem prid2g 4047

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

Syntax hints:   -> wi 4   e. wcel 1890   {cpr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3014  df-un 3376  df-sn 3936  df-pr 3938

This theorem is referenced by:  unisn2  4510  fr2nr  4789  fpr2g  6110  f1prex  6167  pw2f1olem  7662  hashprdifel  12568  gcdcllem3  14485  mgm2nsgrplem1  16662  mgm2nsgrplem2  16663  mgm2nsgrplem3  16664  sgrp2nmndlem1  16667  sgrp2rid2  16670  pmtrprfv  17104  m2detleib  19666  indistopon  20026  pptbas  20033  coseq0negpitopi  23469  usgra2edg  25120  nb3graprlem1  25190  nb3graprlem2  25191  2trllemF  25290  vdgr1b  25643  prsiga  28959  ftc1anclem8  32025  fourierdlem54  38080  prsal  38235  sge0pr  38294  imarnf1pr  39109  uhgr2edg  39390  uspgr2v1e2w  39427  usgr2v1e2w  39428  nb3grprlem1  39555  nb3grprlem2  39556  usgvad2edg  40047