Theorem prid2g 4786

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

Syntax hints:   → wi 4   ∈ wcel 2103  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3484  df-un 3975  df-sn 4649  df-pr 4651

This theorem is referenced by:  prel12g  4888  prproe  4929  unisn2  5333  fr2nr  5677  fpr2g  7246  f1prex  7318  fvf1pr  7340  pw2f1olem  9138  hashprdifel  14443  gcdcllem3  16541  mgm2nsgrplem1  18948  mgm2nsgrplem2  18949  mgm2nsgrplem3  18950  sgrp2nmndlem1  18953  sgrp2rid2  18956  pmtrprfv  19490  m2detleib  22651  indistopon  23022  pptbas  23029  coseq0negpitopi  26555  uhgr2edg  29234  umgrvad2edg  29239  uspgr2v1e2w  29277  usgr2v1e2w  29278  nb3grprlem1  29406  nb3grprlem2  29407  1hegrvtxdg1  29534  cyc3genpmlem  33136  elrspunsn  33414  prsiga  34087  bj-prmoore  37029  ftc1anclem8  37608  pr2el2  43453  pr2eldif2  43457  fourierdlem54  46015  prsal  46173  sge0pr  46249  imarnf1pr  47129  paireqne  47317  1hegrlfgr  47773  lubprlem  48560