Theorem prid1g 4484

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 2799	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 892	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4389	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 250	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 874   = wceq 1653   ∈ wcel 2157  {cpr 4370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-un 3774  df-sn 4369  df-pr 4371

This theorem is referenced by:  prid2g  4485  prid1  4486  prnzg  4499  preq1b  4563  prel12g  4584  elpreqprb  4588  prproe  4626  opth1  5134  fr2nr  5290  fpr2g  6704  f1prex  6767  fveqf1o  6785  pw2f1olem  8306  hashprdifel  13435  gcdcllem3  15558  mgm2nsgrplem1  17721  mgm2nsgrplem2  17722  mgm2nsgrplem3  17723  sgrp2nmndlem1  17726  sgrp2rid2  17729  pmtrprfv  18185  pptbas  21141  coseq0negpitopi  24597  uhgr2edg  26441  umgrvad2edg  26446  uspgr2v1e2w  26485  usgr2v1e2w  26486  nbusgredgeu0  26612  nbusgrf1o0  26613  nb3grprlem1  26624  nb3grprlem2  26625  vtxduhgr0nedg  26742  1hegrvtxdg1  26757  1egrvtxdg1  26759  umgr2v2evd2  26777  vdegp1bi  26787  ftc1anclem8  33980  kelac2  38420  fourierdlem54  41120  sge0pr  41354  imarnf1pr  42137  fmtnoprmfac2lem1  42260  1hegrlfgr  42512