Theorem prid1g 4731

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  prid2g  4732  prid1  4733  prnzg  4749  preq1b  4816  prel12g  4834  elpreqprb  4838  prproe  4875  opth1  5462  fr2nr  5643  fpr2g  7216  f1prex  7293  fveqf1o  7311  fvf1pr  7316  pw2f1olem  9079  hashprdifel  14454  gcdcllem3  16584  mgm2nsgrplem1  19011  mgm2nsgrplem2  19012  mgm2nsgrplem3  19013  sgrp2nmndlem1  19016  sgrp2rid2  19019  pmtrprfv  19554  pptbas  23202  coseq0negpitopi  26705  uhgr2edg  29595  umgrvad2edg  29600  uspgr2v1e2w  29638  usgr2v1e2w  29639  nbusgredgeu0  29755  nbusgrf1o0  29756  nb3grprlem1  29767  nb3grprlem2  29768  vtxduhgr0nedg  29879  1hegrvtxdg1  29894  1egrvtxdg1  29896  umgr2v2evd2  29914  vdegp1bi  29924  mptprop  33080  altgnsg  33500  cyc3genpmlem  33502  elrspunsn  33768  esplyfval1  33994  bj-prmoore  37798  ftc1anclem8  38392  kelac2  43833  pr2el1  44316  pr2eldif1  44321  fourierdlem54  46915  sge0pr  47149  imarnf1pr  48060  paireqne  48301  fmtnoprmfac2lem1  48359  grlimprclnbgr  48802  grlimprclnbgredg  48803  1hegrlfgr  48938  fucoppcffth  50230  termc2  50337  uobeqterm  50365  2arwcatlem4  50417  incat  50420