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  4807  prel12g  4825  elpreqprb  4829  prproe  4866  opth1  5448  fr2nr  5629  fpr2g  7199  f1prex  7272  fveqf1o  7290  fvf1pr  7295  pw2f1olem  9057  hashprdifel  14425  gcdcllem3  16549  mgm2nsgrplem1  18970  mgm2nsgrplem2  18971  mgm2nsgrplem3  18972  sgrp2nmndlem1  18975  sgrp2rid2  18978  pmtrprfv  19514  pptbas  23126  coseq0negpitopi  26626  uhgr2edg  29467  umgrvad2edg  29472  uspgr2v1e2w  29510  usgr2v1e2w  29511  nbusgredgeu0  29627  nbusgrf1o0  29628  nb3grprlem1  29639  nb3grprlem2  29640  vtxduhgr0nedg  29751  1hegrvtxdg1  29766  1egrvtxdg1  29768  umgr2v2evd2  29786  vdegp1bi  29796  mptprop  32955  altgnsg  33382  cyc3genpmlem  33384  elrspunsn  33653  esplyfval1  33880  bj-prmoore  37617  ftc1anclem8  38211  kelac2  43654  pr2el1  44137  pr2eldif1  44142  fourierdlem54  46732  sge0pr  46966  imarnf1pr  47874  paireqne  48115  fmtnoprmfac2lem1  48173  grlimprclnbgr  48616  grlimprclnbgredg  48617  1hegrlfgr  48752  fucoppcffth  50040  termc2  50147  uobeqterm  50175  2arwcatlem4  50227  incat  50230