Theorem prid1g 4648

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1542   ∈ wcel 2113  {cpr 4515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-sn 4514  df-pr 4516

This theorem is referenced by:  prid2g  4649  prid1  4650  prnzg  4666  preq1b  4729  prel12g  4746  elpreqprb  4750  prproe  4791  opth1  5330  fr2nr  5497  fpr2g  6978  f1prex  7045  fveqf1o  7064  pw2f1olem  8663  hashprdifel  13844  gcdcllem3  15937  mgm2nsgrplem1  18192  mgm2nsgrplem2  18193  mgm2nsgrplem3  18194  sgrp2nmndlem1  18197  sgrp2rid2  18200  pmtrprfv  18692  pptbas  21752  coseq0negpitopi  25240  uhgr2edg  27142  umgrvad2edg  27147  uspgr2v1e2w  27185  usgr2v1e2w  27186  nbusgredgeu0  27302  nbusgrf1o0  27303  nb3grprlem1  27314  nb3grprlem2  27315  vtxduhgr0nedg  27426  1hegrvtxdg1  27441  1egrvtxdg1  27443  umgr2v2evd2  27461  vdegp1bi  27471  mptprop  30598  altgnsg  30985  cyc3genpmlem  30987  bj-prmoore  34896  ftc1anclem8  35469  kelac2  40446  pr2el1  40685  pr2eldif1  40690  fourierdlem54  43227  sge0pr  43458  imarnf1pr  44291  paireqne  44481  fmtnoprmfac2lem1  44536  1hegrlfgr  44812