Theorem prid1g 4239

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 2610	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 404	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4144	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 247	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 382   = wceq 1475   ∈ wcel 1977  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  prid2g  4240  prid1  4241  prnzg  4254  preq1b  4317  elpreqprb  4335  opth1  4870  fr2nr  5016  fpr2g  6380  f1prex  6439  fveqf1o  6457  pw2f1olem  7949  hashprdifel  13047  gcdcllem3  15061  mgm2nsgrplem1  17228  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2nmndlem1  17233  sgrp2rid2  17236  pmtrprfv  17696  pptbas  20622  coseq0negpitopi  24059  usgra2edg  25911  nbgraf1olem1  25970  nbgraf1olem3  25972  nbgraf1olem5  25974  nb3graprlem1  25980  nb3graprlem2  25981  constr1trl  26118  vdgr1b  26431  vdusgra0nedg  26435  usgravd0nedg  26445  vdn0frgrav2  26550  vdgn0frgrav2  26551  ftc1anclem8  32662  kelac2  36653  fourierdlem54  39053  sge0pr  39287  fmtnoprmfac2lem1  40016  imarnf1pr  40326  uhgr2edg  40435  umgrvad2edg  40440  uspgr2v1e2w  40477  usgr2v1e2w  40478  nbusgredgeu0  40596  nbusgrf1o0  40597  nb3grprlem1  40608  nb3grprlem2  40609  vtxduhgr0nedg  40707  1hegrlfgr  40722  1hegrvtxdg1  40723  1egrvtxdg1  40725  umgr2v2evd2  40743  vdegp1bi-av  40753