Theorem prid2g 4657

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	⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Proof of Theorem prid2g

Step	Hyp	Ref	Expression
1		prid1g 4656	. 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴})
2		prcom 4628	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
3	1, 2	eleqtrdi 2900	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∈ wcel 2111  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  prel12g  4754  prproe  4798  unisn2  5180  fr2nr  5497  fpr2g  6951  f1prex  7018  pw2f1olem  8604  hashprdifel  13755  gcdcllem3  15840  mgm2nsgrplem1  18075  mgm2nsgrplem2  18076  mgm2nsgrplem3  18077  sgrp2nmndlem1  18080  sgrp2rid2  18083  pmtrprfv  18573  m2detleib  21236  indistopon  21606  pptbas  21613  coseq0negpitopi  25096  uhgr2edg  26998  umgrvad2edg  27003  uspgr2v1e2w  27041  usgr2v1e2w  27042  nb3grprlem1  27170  nb3grprlem2  27171  1hegrvtxdg1  27297  cyc3genpmlem  30843  prsiga  31500  bj-prmoore  34530  ftc1anclem8  35137  pr2el2  40250  pr2eldif2  40254  fourierdlem54  42802  prsal  42960  sge0pr  43033  imarnf1pr  43838  paireqne  44028  1hegrlfgr  44360