Theorem prid1g 4713

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 2731	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 865	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4599	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  prid2g  4714  prid1  4715  prnzg  4731  preq1b  4798  prel12g  4816  elpreqprb  4820  prproe  4857  opth1  5415  fr2nr  5593  fpr2g  7145  f1prex  7218  fveqf1o  7236  fvf1pr  7241  pw2f1olem  8994  hashprdifel  14302  gcdcllem3  16409  mgm2nsgrplem1  18823  mgm2nsgrplem2  18824  mgm2nsgrplem3  18825  sgrp2nmndlem1  18828  sgrp2rid2  18831  pmtrprfv  19363  pptbas  22921  coseq0negpitopi  26437  uhgr2edg  29184  umgrvad2edg  29189  uspgr2v1e2w  29227  usgr2v1e2w  29228  nbusgredgeu0  29344  nbusgrf1o0  29345  nb3grprlem1  29356  nb3grprlem2  29357  vtxduhgr0nedg  29469  1hegrvtxdg1  29484  1egrvtxdg1  29486  umgr2v2evd2  29504  vdegp1bi  29514  mptprop  32674  altgnsg  33113  cyc3genpmlem  33115  elrspunsn  33389  bj-prmoore  37148  ftc1anclem8  37739  kelac2  43097  pr2el1  43581  pr2eldif1  43586  fourierdlem54  46197  sge0pr  46431  imarnf1pr  47312  paireqne  47541  fmtnoprmfac2lem1  47596  grlimprclnbgr  48026  grlimprclnbgredg  48027  1hegrlfgr  48162  fucoppcffth  49442  termc2  49549  uobeqterm  49577  2arwcatlem4  49629  incat  49632