Theorem prid2g 4743

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

Syntax hints:   → wi 4   ∈ wcel 2107  {cpr 4610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938  df-sn 4609  df-pr 4611

This theorem is referenced by:  prel12g  4846  prproe  4887  unisn2  5294  fr2nr  5644  fpr2g  7214  f1prex  7287  fvf1pr  7310  pw2f1olem  9099  hashprdifel  14420  gcdcllem3  16521  mgm2nsgrplem1  18905  mgm2nsgrplem2  18906  mgm2nsgrplem3  18907  sgrp2nmndlem1  18910  sgrp2rid2  18913  pmtrprfv  19444  m2detleib  22604  indistopon  22974  pptbas  22981  coseq0negpitopi  26500  uhgr2edg  29172  umgrvad2edg  29177  uspgr2v1e2w  29215  usgr2v1e2w  29216  nb3grprlem1  29344  nb3grprlem2  29345  1hegrvtxdg1  29472  cyc3genpmlem  33117  elrspunsn  33398  prsiga  34073  bj-prmoore  37057  ftc1anclem8  37648  pr2el2  43509  pr2eldif2  43513  fourierdlem54  46120  prsal  46278  sge0pr  46354  imarnf1pr  47240  paireqne  47444  stgrnbgr0  47877  1hegrlfgr  47994  lubprlem  48807