Theorem prid2g 4761

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 4760	. 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴})
2		prcom 4732	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
3	1, 2	eleqtrdi 2838	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∈ wcel 2099  {cpr 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-un 3949  df-sn 4625  df-pr 4627

This theorem is referenced by:  prel12g  4860  prproe  4901  unisn2  5306  fr2nr  5650  fpr2g  7217  f1prex  7287  pw2f1olem  9092  hashprdifel  14381  gcdcllem3  16467  mgm2nsgrplem1  18861  mgm2nsgrplem2  18862  mgm2nsgrplem3  18863  sgrp2nmndlem1  18866  sgrp2rid2  18869  pmtrprfv  19399  m2detleib  22520  indistopon  22891  pptbas  22898  coseq0negpitopi  26425  uhgr2edg  29008  umgrvad2edg  29013  uspgr2v1e2w  29051  usgr2v1e2w  29052  nb3grprlem1  29180  nb3grprlem2  29181  1hegrvtxdg1  29308  cyc3genpmlem  32850  elrspunsn  33080  prsiga  33686  bj-prmoore  36530  ftc1anclem8  37108  pr2el2  42904  pr2eldif2  42908  fourierdlem54  45471  prsal  45629  sge0pr  45705  imarnf1pr  46585  paireqne  46774  1hegrlfgr  47117  lubprlem  47904