Theorem prid2g 4727

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

Syntax hints:   → wi 4   ∈ wcel 2143  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is referenced by:  prel12g  4829  prproe  4870  unisn2  5275  fr2nr  5638  fpr2g  7209  f1prex  7282  fvf1pr  7305  pw2f1olem  9065  hashprdifel  14430  gcdcllem3  16554  chnccat  18677  mgm2nsgrplem1  18975  mgm2nsgrplem2  18976  mgm2nsgrplem3  18977  sgrp2nmndlem1  18980  sgrp2rid2  18983  pmtrprfv  19518  m2detleib  22788  indistopon  23158  pptbas  23165  coseq0negpitopi  26668  uhgr2edg  29558  umgrvad2edg  29563  uspgr2v1e2w  29601  usgr2v1e2w  29602  nb3grprlem1  29730  nb3grprlem2  29731  1hegrvtxdg1  29857  cyc3genpmlem  33471  elrspunsn  33737  esplyfval1  33963  prsiga  34521  bj-prmoore  37777  ftc1anclem8  38371  pr2el2  44297  pr2eldif2  44301  fourierdlem54  46894  prsal  47052  sge0pr  47128  imarnf1pr  48039  paireqne  48280  stgrnbgr0  48749  grlimprclnbgr  48781  1hegrlfgr  48917  lubprlem  49760  fucoppcffth  50209  uobeqterm  50344  2arwcatlem4  50396  2arwcat  50398  incat  50399