Theorem prid1g 4721

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  prid2g  4722  prid1  4723  prnzg  4739  preq1b  4806  prel12g  4824  elpreqprb  4828  prproe  4865  opth1  5444  fr2nr  5628  fpr2g  7209  f1prex  7284  fveqf1o  7302  fvf1pr  7307  pw2f1olem  9084  hashprdifel  14522  gcdcllem3  16651  mgm2nsgrplem1  19097  mgm2nsgrplem2  19098  mgm2nsgrplem3  19099  sgrp2nmndlem1  19102  sgrp2rid2  19105  pmtrprfv  19647  pptbas  23306  coseq0negpitopi  26814  uhgr2edg  29771  umgrvad2edg  29776  uspgr2v1e2w  29814  usgr2v1e2w  29815  nbusgredgeu0  29931  nbusgrf1o0  29932  nb3grprlem1  29943  nb3grprlem2  29944  vtxduhgr0nedg  30055  1hegrvtxdg1  30070  1egrvtxdg1  30072  umgr2v2evd2  30090  vdegp1bi  30100  mptprop  33273  altgnsg  33692  cyc3genpmlem  33694  elrspunsn  33961  esplyfval1  34187  bj-prmoore  38004  ftc1anclem8  38586  kelac2  44025  pr2el1  44508  pr2eldif1  44513  fourierdlem54  47114  sge0pr  47348  imarnf1pr  48296  paireqne  48537  fmtnoprmfac2lem1  48595  grlimprclnbgr  49038  grlimprclnbgredg  49039  1hegrlfgr  49174  fucoppcffth  50463  termc2  50570  uobeqterm  50598  2arwcatlem4  50650  incat  50653