Theorem prid1g 4717

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)

Assertion

Ref	Expression
prid1g	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Proof of Theorem prid1g

Step	Hyp	Ref	Expression
1		eqid 2736	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 865	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4603	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  prid2g  4718  prid1  4719  prnzg  4735  preq1b  4802  prel12g  4820  elpreqprb  4824  prproe  4861  opth1  5423  fr2nr  5601  fpr2g  7157  f1prex  7230  fveqf1o  7248  fvf1pr  7253  pw2f1olem  9009  hashprdifel  14321  gcdcllem3  16428  mgm2nsgrplem1  18843  mgm2nsgrplem2  18844  mgm2nsgrplem3  18845  sgrp2nmndlem1  18848  sgrp2rid2  18851  pmtrprfv  19382  pptbas  22952  coseq0negpitopi  26468  uhgr2edg  29281  umgrvad2edg  29286  uspgr2v1e2w  29324  usgr2v1e2w  29325  nbusgredgeu0  29441  nbusgrf1o0  29442  nb3grprlem1  29453  nb3grprlem2  29454  vtxduhgr0nedg  29566  1hegrvtxdg1  29581  1egrvtxdg1  29583  umgr2v2evd2  29601  vdegp1bi  29611  mptprop  32777  altgnsg  33231  cyc3genpmlem  33233  elrspunsn  33510  bj-prmoore  37316  ftc1anclem8  37897  kelac2  43303  pr2el1  43786  pr2eldif1  43791  fourierdlem54  46400  sge0pr  46634  imarnf1pr  47524  paireqne  47753  fmtnoprmfac2lem1  47808  grlimprclnbgr  48238  grlimprclnbgredg  48239  1hegrlfgr  48374  fucoppcffth  49652  termc2  49759  uobeqterm  49787  2arwcatlem4  49839  incat  49842