Theorem prid1g 4656

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

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  prid2g  4657  prid1  4658  prnzg  4674  preq1b  4737  prel12g  4754  elpreqprb  4758  prproe  4798  opth1  5332  fr2nr  5497  fpr2g  6951  f1prex  7018  fveqf1o  7037  pw2f1olem  8604  hashprdifel  13755  gcdcllem3  15840  mgm2nsgrplem1  18075  mgm2nsgrplem2  18076  mgm2nsgrplem3  18077  sgrp2nmndlem1  18080  sgrp2rid2  18083  pmtrprfv  18573  pptbas  21613  coseq0negpitopi  25096  uhgr2edg  26998  umgrvad2edg  27003  uspgr2v1e2w  27041  usgr2v1e2w  27042  nbusgredgeu0  27158  nbusgrf1o0  27159  nb3grprlem1  27170  nb3grprlem2  27171  vtxduhgr0nedg  27282  1hegrvtxdg1  27297  1egrvtxdg1  27299  umgr2v2evd2  27317  vdegp1bi  27327  mptprop  30458  altgnsg  30841  cyc3genpmlem  30843  bj-prmoore  34530  ftc1anclem8  35137  kelac2  40009  pr2el1  40248  pr2eldif1  40253  fourierdlem54  42802  sge0pr  43033  imarnf1pr  43838  paireqne  44028  fmtnoprmfac2lem1  44083  1hegrlfgr  44360