Theorem prid1g 4763

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  prid2g  4764  prid1  4765  prnzg  4781  preq1b  4846  prel12g  4863  elpreqprb  4867  prproe  4905  opth1  5474  fr2nr  5653  fpr2g  7208  f1prex  7277  fveqf1o  7296  pw2f1olem  9072  hashprdifel  14354  gcdcllem3  16438  mgm2nsgrplem1  18795  mgm2nsgrplem2  18796  mgm2nsgrplem3  18797  sgrp2nmndlem1  18800  sgrp2rid2  18803  pmtrprfv  19314  pptbas  22493  coseq0negpitopi  25995  uhgr2edg  28445  umgrvad2edg  28450  uspgr2v1e2w  28488  usgr2v1e2w  28489  nbusgredgeu0  28605  nbusgrf1o0  28606  nb3grprlem1  28617  nb3grprlem2  28618  vtxduhgr0nedg  28729  1hegrvtxdg1  28744  1egrvtxdg1  28746  umgr2v2evd2  28764  vdegp1bi  28774  mptprop  31898  altgnsg  32286  cyc3genpmlem  32288  elrspunsn  32505  bj-prmoore  35934  ftc1anclem8  36506  kelac2  41740  pr2el1  42233  pr2eldif1  42238  fourierdlem54  44811  sge0pr  45045  imarnf1pr  45925  paireqne  46114  fmtnoprmfac2lem1  46169  1hegrlfgr  46445