Theorem prid1g 4717

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 879	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4603	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  prid2g  4718  prid1  4719  prnzg  4735  preq1b  4800  prel12g  4818  elpreqprb  4822  prproe  4832  opth1  5443  fr2nr  5627  fpr2g  7218  f1prex  7293  fveqf1o  7311  fvf1pr  7316  pw2f1olem  9104  hashprdifel  14546  gcdcllem3  16677  mgm2nsgrplem1  19123  mgm2nsgrplem2  19124  mgm2nsgrplem3  19125  sgrp2nmndlem1  19128  sgrp2rid2  19131  pmtrprfv  19673  pptbas  23332  coseq0negpitopi  26838  uhgr2edg  29795  umgrvad2edg  29800  uspgr2v1e2w  29838  usgr2v1e2w  29839  nbusgredgeu0  29955  nbusgrf1o0  29956  nb3grprlem1  29967  nb3grprlem2  29968  vtxduhgr0nedg  30079  1hegrvtxdg1  30094  1egrvtxdg1  30096  umgr2v2evd2  30114  vdegp1bi  30124  mptprop  33339  altgnsg  33757  cyc3genpmlem  33759  elrspunsn  34026  esplyfval1  34252  bj-prmoore  38129  ftc1anclem8  38712  kelac2  44161  pr2el1  44644  pr2eldif1  44649  fourierdlem54  47264  sge0pr  47498  imarnf1pr  48446  paireqne  48687  fmtnoprmfac2lem1  48745  grlimprclnbgr  49188  grlimprclnbgredg  49189  1hegrlfgr  49324  line2  49958  fucoppcffth  50640  termc2  50747  uobeqterm  50778  2arwcatlem4  50830  incat  50833