Theorem prid1g 4295

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

Syntax hints:   → wi 4   ∨ wo 383   = wceq 1483   ∈ wcel 1990  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  prid2g  4296  prid1  4297  prnzg  4311  preq1b  4377  elpreqprb  4397  prproe  4434  opth1  4944  fr2nr  5092  fpr2g  6475  f1prex  6539  fveqf1o  6557  pw2f1olem  8064  hashprdifel  13186  gcdcllem3  15223  mgm2nsgrplem1  17405  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2nmndlem1  17410  sgrp2rid2  17413  pmtrprfv  17873  pptbas  20812  coseq0negpitopi  24255  uhgr2edg  26100  umgrvad2edg  26105  uspgr2v1e2w  26143  usgr2v1e2w  26144  nbusgredgeu0  26270  nbusgrf1o0  26271  nb3grprlem1  26282  nb3grprlem2  26283  vtxduhgr0nedg  26388  1hegrvtxdg1  26403  1egrvtxdg1  26405  umgr2v2evd2  26423  vdegp1bi  26433  ftc1anclem8  33492  kelac2  37635  fourierdlem54  40377  sge0pr  40611  imarnf1pr  41301  fmtnoprmfac2lem1  41478  1hegrlfgr  41713