Theorem prid1g 4722

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 2765	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 878	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4608	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1563   ∈ wcel 2145  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  prid2g  4723  prid1  4724  prnzg  4740  preq1b  4806  prel12g  4824  elpreqprb  4828  prproe  4865  opth1  5447  fr2nr  5628  fpr2g  7199  f1prex  7272  fveqf1o  7290  fvf1pr  7295  pw2f1olem  9057  hashprdifel  14422  gcdcllem3  16547  mgm2nsgrplem1  18968  mgm2nsgrplem2  18969  mgm2nsgrplem3  18970  sgrp2nmndlem1  18973  sgrp2rid2  18976  pmtrprfv  19511  pptbas  23122  coseq0negpitopi  26622  uhgr2edg  29463  umgrvad2edg  29468  uspgr2v1e2w  29506  usgr2v1e2w  29507  nbusgredgeu0  29623  nbusgrf1o0  29624  nb3grprlem1  29635  nb3grprlem2  29636  vtxduhgr0nedg  29747  1hegrvtxdg1  29762  1egrvtxdg1  29764  umgr2v2evd2  29782  vdegp1bi  29792  mptprop  32951  altgnsg  33377  cyc3genpmlem  33379  elrspunsn  33648  esplyfval1  33875  bj-prmoore  37612  ftc1anclem8  38206  kelac2  43649  pr2el1  44132  pr2eldif1  44137  fourierdlem54  46733  sge0pr  46967  imarnf1pr  47875  paireqne  48116  fmtnoprmfac2lem1  48174  grlimprclnbgr  48617  grlimprclnbgredg  48618  1hegrlfgr  48753  fucoppcffth  50041  termc2  50148  uobeqterm  50176  2arwcatlem4  50228  incat  50231