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 2763	. . 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 2147  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  prid2g  4722  prid1  4723  prnzg  4739  preq1b  4804  prel12g  4822  elpreqprb  4826  prproe  4836  opth1  5449  fr2nr  5633  fpr2g  7243  f1prex  7318  fveqf1o  7336  fvf1pr  7341  pw2f1olem  9131  hashprdifel  14572  gcdcllem3  16703  mgm2nsgrplem1  19149  mgm2nsgrplem2  19150  mgm2nsgrplem3  19151  sgrp2nmndlem1  19154  sgrp2rid2  19157  pmtrprfv  19700  pptbas  23359  coseq0negpitopi  26865  uhgr2edg  29822  umgrvad2edg  29827  uspgr2v1e2w  29865  usgr2v1e2w  29866  nbusgredgeu0  29982  nbusgrf1o0  29983  nb3grprlem1  29994  nb3grprlem2  29995  vtxduhgr0nedg  30106  1hegrvtxdg1  30121  1egrvtxdg1  30123  umgr2v2evd2  30141  vdegp1bi  30151  mptprop  33365  altgnsg  33786  cyc3genpmlem  33788  elrspunsn  34063  esplyfval1  34288  bj-prmoore  38240  ftc1anclem8  38823  kelac2  44271  pr2el1  44753  pr2eldif1  44758  fourierdlem54  47385  sge0pr  47619  imarnf1pr  48567  paireqne  48808  fmtnoprmfac2lem1  48866  grlimprclnbgr  49309  grlimprclnbgredg  49310  1hegrlfgr  49445  line2  50079  fucoppcffth  50761  termc2  50868  uobeqterm  50899  2arwcatlem4  50951  incat  50954