Theorem prid2g 4694

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  prel12g  4791  prproe  4834  unisn2  5231  fr2nr  5558  fpr2g  7069  f1prex  7136  pw2f1olem  8816  hashprdifel  14041  gcdcllem3  16136  mgm2nsgrplem1  18472  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2nmndlem1  18477  sgrp2rid2  18480  pmtrprfv  18976  m2detleib  21688  indistopon  22059  pptbas  22066  coseq0negpitopi  25565  uhgr2edg  27478  umgrvad2edg  27483  uspgr2v1e2w  27521  usgr2v1e2w  27522  nb3grprlem1  27650  nb3grprlem2  27651  1hegrvtxdg1  27777  cyc3genpmlem  31320  prsiga  31999  bj-prmoore  35213  ftc1anclem8  35784  pr2el2  41047  pr2eldif2  41051  fourierdlem54  43591  prsal  43749  sge0pr  43822  imarnf1pr  44661  paireqne  44851  1hegrlfgr  45182  lubprlem  46144