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 2871	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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  prel12g  4824  prproe  4865  unisn2  5266  fr2nr  5628  fpr2g  7217  f1prex  7292  fvf1pr  7315  pw2f1olem  9100  hashprdifel  14542  gcdcllem3  16671  chnccat  18800  mgm2nsgrplem1  19117  mgm2nsgrplem2  19118  mgm2nsgrplem3  19119  sgrp2nmndlem1  19122  sgrp2rid2  19125  pmtrprfv  19667  m2detleib  22946  indistopon  23319  pptbas  23326  coseq0negpitopi  26832  uhgr2edg  29789  umgrvad2edg  29794  uspgr2v1e2w  29832  usgr2v1e2w  29833  nb3grprlem1  29961  nb3grprlem2  29962  1hegrvtxdg1  30088  cyc3genpmlem  33712  elrspunsn  33979  esplyfval1  34205  prsiga  34763  bj-prmoore  38036  ftc1anclem8  38618  pr2el2  44551  pr2eldif2  44555  fourierdlem54  47169  prsal  47327  sge0pr  47403  imarnf1pr  48351  paireqne  48592  stgrnbgr0  49061  grlimprclnbgr  49093  1hegrlfgr  49229  lubprlem  50069  fucoppcffth  50518  uobeqterm  50653  2arwcatlem4  50705  2arwcat  50707  incat  50708