Theorem prid1g 4712

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4576  df-pr 4578

This theorem is referenced by:  prid2g  4713  prid1  4714  prnzg  4730  preq1b  4797  prel12g  4815  elpreqprb  4819  prproe  4856  opth1  5418  fr2nr  5596  fpr2g  7151  f1prex  7224  fveqf1o  7242  fvf1pr  7247  pw2f1olem  9001  hashprdifel  14307  gcdcllem3  16414  mgm2nsgrplem1  18828  mgm2nsgrplem2  18829  mgm2nsgrplem3  18830  sgrp2nmndlem1  18833  sgrp2rid2  18836  pmtrprfv  19367  pptbas  22924  coseq0negpitopi  26440  uhgr2edg  29188  umgrvad2edg  29193  uspgr2v1e2w  29231  usgr2v1e2w  29232  nbusgredgeu0  29348  nbusgrf1o0  29349  nb3grprlem1  29360  nb3grprlem2  29361  vtxduhgr0nedg  29473  1hegrvtxdg1  29488  1egrvtxdg1  29490  umgr2v2evd2  29508  vdegp1bi  29518  mptprop  32683  altgnsg  33125  cyc3genpmlem  33127  elrspunsn  33401  bj-prmoore  37180  ftc1anclem8  37760  kelac2  43182  pr2el1  43666  pr2eldif1  43671  fourierdlem54  46282  sge0pr  46516  imarnf1pr  47406  paireqne  47635  fmtnoprmfac2lem1  47690  grlimprclnbgr  48120  grlimprclnbgredg  48121  1hegrlfgr  48256  fucoppcffth  49536  termc2  49643  uobeqterm  49671  2arwcatlem4  49723  incat  49726