Theorem prid2g 4694

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

Syntax hints:   → wi 4   ∈ wcel 2119  {cpr 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4557  df-pr 4559

This theorem is referenced by:  prel12g  4796  prproe  4837  unisn2  5235  fr2nr  5596  fpr2g  7156  f1prex  7229  fvf1pr  7252  pw2f1olem  9010  hashprdifel  14352  gcdcllem3  16462  chnccat  18584  mgm2nsgrplem1  18881  mgm2nsgrplem2  18882  mgm2nsgrplem3  18883  sgrp2nmndlem1  18886  sgrp2rid2  18889  pmtrprfv  19420  m2detleib  22615  indistopon  22985  pptbas  22992  coseq0negpitopi  26486  uhgr2edg  29296  umgrvad2edg  29301  uspgr2v1e2w  29339  usgr2v1e2w  29340  nb3grprlem1  29468  nb3grprlem2  29469  1hegrvtxdg1  29595  cyc3genpmlem  33233  elrspunsn  33513  esplyfval1  33766  prsiga  34324  bj-prmoore  37482  ftc1anclem8  38076  pr2el2  44004  pr2eldif2  44008  fourierdlem54  46611  prsal  46769  sge0pr  46845  imarnf1pr  47753  paireqne  47994  stgrnbgr0  48463  grlimprclnbgr  48495  1hegrlfgr  48631  lubprlem  49460  fucoppcffth  49909  uobeqterm  50044  2arwcatlem4  50096  2arwcat  50098  incat  50099