Theorem prid2g 4711

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  prel12g  4813  prproe  4854  unisn2  5248  fr2nr  5591  fpr2g  7145  f1prex  7218  fvf1pr  7241  pw2f1olem  8994  hashprdifel  14305  gcdcllem3  16412  chnccat  18532  mgm2nsgrplem1  18826  mgm2nsgrplem2  18827  mgm2nsgrplem3  18828  sgrp2nmndlem1  18831  sgrp2rid2  18834  pmtrprfv  19365  m2detleib  22546  indistopon  22916  pptbas  22923  coseq0negpitopi  26439  uhgr2edg  29186  umgrvad2edg  29191  uspgr2v1e2w  29229  usgr2v1e2w  29230  nb3grprlem1  29358  nb3grprlem2  29359  1hegrvtxdg1  29486  cyc3genpmlem  33120  elrspunsn  33394  prsiga  34144  bj-prmoore  37159  ftc1anclem8  37750  pr2el2  43654  pr2eldif2  43658  fourierdlem54  46268  prsal  46426  sge0pr  46502  imarnf1pr  47392  paireqne  47621  stgrnbgr0  48074  grlimprclnbgr  48106  1hegrlfgr  48242  lubprlem  49072  fucoppcffth  49522  uobeqterm  49657  2arwcatlem4  49709  2arwcat  49711  incat  49712