Theorem prid2g 4732

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  prel12g  4834  prproe  4875  unisn2  5280  fr2nr  5643  fpr2g  7216  f1prex  7293  fvf1pr  7316  pw2f1olem  9079  hashprdifel  14454  gcdcllem3  16584  chnccat  18707  mgm2nsgrplem1  19005  mgm2nsgrplem2  19006  mgm2nsgrplem3  19007  sgrp2nmndlem1  19010  sgrp2rid2  19013  pmtrprfv  19548  m2detleib  22818  indistopon  23188  pptbas  23195  coseq0negpitopi  26698  uhgr2edg  29588  umgrvad2edg  29593  uspgr2v1e2w  29631  usgr2v1e2w  29632  nb3grprlem1  29760  nb3grprlem2  29761  1hegrvtxdg1  29887  cyc3genpmlem  33495  elrspunsn  33761  esplyfval1  33987  prsiga  34545  bj-prmoore  37790  ftc1anclem8  38384  pr2el2  44310  pr2eldif2  44314  fourierdlem54  46907  prsal  47065  sge0pr  47141  imarnf1pr  48052  paireqne  48293  stgrnbgr0  48762  grlimprclnbgr  48794  1hegrlfgr  48930  lubprlem  49773  fucoppcffth  50222  uobeqterm  50357  2arwcatlem4  50409  2arwcat  50411  incat  50412