Theorem prid1g 4704

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  prid2g  4705  prid1  4706  prnzg  4722  preq1b  4789  prel12g  4807  elpreqprb  4811  prproe  4848  opth1  5428  fr2nr  5608  fpr2g  7166  f1prex  7239  fveqf1o  7257  fvf1pr  7262  pw2f1olem  9019  hashprdifel  14360  gcdcllem3  16470  mgm2nsgrplem1  18889  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2nmndlem1  18894  sgrp2rid2  18897  pmtrprfv  19428  pptbas  22973  coseq0negpitopi  26467  uhgr2edg  29277  umgrvad2edg  29282  uspgr2v1e2w  29320  usgr2v1e2w  29321  nbusgredgeu0  29437  nbusgrf1o0  29438  nb3grprlem1  29449  nb3grprlem2  29450  vtxduhgr0nedg  29561  1hegrvtxdg1  29576  1egrvtxdg1  29578  umgr2v2evd2  29596  vdegp1bi  29606  mptprop  32771  altgnsg  33210  cyc3genpmlem  33212  elrspunsn  33489  esplyfval1  33717  bj-prmoore  37427  ftc1anclem8  38021  kelac2  43493  pr2el1  43976  pr2eldif1  43981  fourierdlem54  46588  sge0pr  46822  imarnf1pr  47730  paireqne  47971  fmtnoprmfac2lem1  48029  grlimprclnbgr  48472  grlimprclnbgredg  48473  1hegrlfgr  48608  fucoppcffth  49886  termc2  49993  uobeqterm  50021  2arwcatlem4  50073  incat  50076