Theorem prid1g 4724

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  prid2g  4725  prid1  4726  prnzg  4742  preq1b  4810  prel12g  4828  elpreqprb  4832  prproe  4869  opth1  5435  fr2nr  5615  fpr2g  7185  f1prex  7259  fveqf1o  7277  fvf1pr  7282  pw2f1olem  9045  hashprdifel  14363  gcdcllem3  16471  mgm2nsgrplem1  18845  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem1  18850  sgrp2rid2  18853  pmtrprfv  19383  pptbas  22895  coseq0negpitopi  26412  uhgr2edg  29135  umgrvad2edg  29140  uspgr2v1e2w  29178  usgr2v1e2w  29179  nbusgredgeu0  29295  nbusgrf1o0  29296  nb3grprlem1  29307  nb3grprlem2  29308  vtxduhgr0nedg  29420  1hegrvtxdg1  29435  1egrvtxdg1  29437  umgr2v2evd2  29455  vdegp1bi  29465  mptprop  32621  altgnsg  33106  cyc3genpmlem  33108  elrspunsn  33400  bj-prmoore  37103  ftc1anclem8  37694  kelac2  43054  pr2el1  43538  pr2eldif1  43543  fourierdlem54  46158  sge0pr  46392  imarnf1pr  47283  paireqne  47512  fmtnoprmfac2lem1  47567  1hegrlfgr  48120  fucoppcffth  49400  termc2  49507  uobeqterm  49535  2arwcatlem4  49587  incat  49590