Theorem prid2g 4296

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 4295	. 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴})
2		prcom 4267	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
3	1, 2	syl6eleq 2711	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∈ wcel 1990  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  prproe  4434  unisn2  4794  fr2nr  5092  fpr2g  6475  f1prex  6539  pw2f1olem  8064  hashprdifel  13186  gcdcllem3  15223  mgm2nsgrplem1  17405  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2nmndlem1  17410  sgrp2rid2  17413  pmtrprfv  17873  m2detleib  20437  indistopon  20805  pptbas  20812  coseq0negpitopi  24255  uhgr2edg  26100  umgrvad2edg  26105  uspgr2v1e2w  26143  usgr2v1e2w  26144  nb3grprlem1  26282  nb3grprlem2  26283  1hegrvtxdg1  26403  prsiga  30194  ftc1anclem8  33492  fourierdlem54  40377  prsal  40538  sge0pr  40611  imarnf1pr  41301  1hegrlfgr  41713