Theorem prid2g 4722

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  prel12g  4822  prproe  4836  unisn2  5269  fr2nr  5632  fpr2g  7227  f1prex  7302  fvf1pr  7325  pw2f1olem  9114  hashprdifel  14555  gcdcllem3  16686  chnccat  18815  mgm2nsgrplem1  19132  mgm2nsgrplem2  19133  mgm2nsgrplem3  19134  sgrp2nmndlem1  19137  sgrp2rid2  19140  pmtrprfv  19682  m2detleib  22961  indistopon  23334  pptbas  23341  coseq0negpitopi  26847  uhgr2edg  29804  umgrvad2edg  29809  uspgr2v1e2w  29847  usgr2v1e2w  29848  nb3grprlem1  29976  nb3grprlem2  29977  1hegrvtxdg1  30103  cyc3genpmlem  33768  elrspunsn  34035  esplyfval1  34261  prsiga  34819  bj-prmoore  38178  ftc1anclem8  38761  pr2el2  44695  pr2eldif2  44699  fourierdlem54  47312  prsal  47470  sge0pr  47546  imarnf1pr  48494  paireqne  48735  stgrnbgr0  49204  grlimprclnbgr  49236  1hegrlfgr  49372  line2  50006  lubprlem  50218  fucoppcffth  50688  uobeqterm  50826  2arwcatlem4  50878  2arwcat  50880  incat  50881