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 2870	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {cpr 4586

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  prel12g  4824  prproe  4865  unisn2  5269  fr2nr  5632  fpr2g  7211  f1prex  7286  fvf1pr  7309  pw2f1olem  9082  hashprdifel  14465  gcdcllem3  16594  chnccat  18717  mgm2nsgrplem1  19033  mgm2nsgrplem2  19034  mgm2nsgrplem3  19035  sgrp2nmndlem1  19038  sgrp2rid2  19041  pmtrprfv  19583  m2detleib  22856  indistopon  23229  pptbas  23236  coseq0negpitopi  26744  uhgr2edg  29671  umgrvad2edg  29676  uspgr2v1e2w  29714  usgr2v1e2w  29715  nb3grprlem1  29843  nb3grprlem2  29844  1hegrvtxdg1  29970  cyc3genpmlem  33594  elrspunsn  33860  esplyfval1  34086  prsiga  34644  bj-prmoore  37868  ftc1anclem8  38452  pr2el2  44394  pr2eldif2  44398  fourierdlem54  46991  prsal  47149  sge0pr  47225  imarnf1pr  48173  paireqne  48414  stgrnbgr0  48883  grlimprclnbgr  48915  1hegrlfgr  49051  lubprlem  49891  fucoppcffth  50340  uobeqterm  50475  2arwcatlem4  50527  2arwcat  50529  incat  50530