Theorem prid1g 4439

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 2760	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 404	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4341	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 248	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 382   = wceq 1632   ∈ wcel 2139  {cpr 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-sn 4322  df-pr 4324

This theorem is referenced by:  prid2g  4440  prid1  4441  prnzg  4454  preq1b  4522  prel12g  4544  elpreqprb  4548  prproe  4586  opth1  5092  fr2nr  5244  fpr2g  6639  f1prex  6702  fveqf1o  6720  pw2f1olem  8229  hashprdifel  13378  gcdcllem3  15425  mgm2nsgrplem1  17606  mgm2nsgrplem2  17607  mgm2nsgrplem3  17608  sgrp2nmndlem1  17611  sgrp2rid2  17614  pmtrprfv  18073  pptbas  21014  coseq0negpitopi  24454  uhgr2edg  26299  umgrvad2edg  26304  uspgr2v1e2w  26342  usgr2v1e2w  26343  nbusgredgeu0  26468  nbusgrf1o0  26469  nb3grprlem1  26480  nb3grprlem2  26481  vtxduhgr0nedg  26598  1hegrvtxdg1  26613  1egrvtxdg1  26615  umgr2v2evd2  26633  vdegp1bi  26643  ftc1anclem8  33805  kelac2  38137  fourierdlem54  40880  sge0pr  41114  imarnf1pr  41809  fmtnoprmfac2lem1  41988  1hegrlfgr  42223