Theorem prid1g 4693

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 861	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4579	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 257	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2108  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  prid2g  4694  prid1  4695  prnzg  4711  preq1b  4774  prel12g  4791  elpreqprb  4795  prproe  4834  opth1  5384  fr2nr  5558  fpr2g  7069  f1prex  7136  fveqf1o  7155  pw2f1olem  8816  hashprdifel  14041  gcdcllem3  16136  mgm2nsgrplem1  18472  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2nmndlem1  18477  sgrp2rid2  18480  pmtrprfv  18976  pptbas  22066  coseq0negpitopi  25565  uhgr2edg  27478  umgrvad2edg  27483  uspgr2v1e2w  27521  usgr2v1e2w  27522  nbusgredgeu0  27638  nbusgrf1o0  27639  nb3grprlem1  27650  nb3grprlem2  27651  vtxduhgr0nedg  27762  1hegrvtxdg1  27777  1egrvtxdg1  27779  umgr2v2evd2  27797  vdegp1bi  27807  mptprop  30933  altgnsg  31318  cyc3genpmlem  31320  bj-prmoore  35213  ftc1anclem8  35784  kelac2  40806  pr2el1  41045  pr2eldif1  41050  fourierdlem54  43591  sge0pr  43822  imarnf1pr  44661  paireqne  44851  fmtnoprmfac2lem1  44906  1hegrlfgr  45182