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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145  {cpr 4589

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  prid2g  4725  prid1  4726  prnzg  4742  preq1b  4809  prel12g  4827  elpreqprb  4831  prproe  4868  opth1  5455  fr2nr  5636  fpr2g  7214  f1prex  7289  fveqf1o  7307  fvf1pr  7312  pw2f1olem  9083  hashprdifel  14466  gcdcllem3  16597  mgm2nsgrplem1  19036  mgm2nsgrplem2  19037  mgm2nsgrplem3  19038  sgrp2nmndlem1  19041  sgrp2rid2  19044  pmtrprfv  19586  pptbas  23239  coseq0negpitopi  26748  uhgr2edg  29676  umgrvad2edg  29681  uspgr2v1e2w  29719  usgr2v1e2w  29720  nbusgredgeu0  29836  nbusgrf1o0  29837  nb3grprlem1  29848  nb3grprlem2  29849  vtxduhgr0nedg  29960  1hegrvtxdg1  29975  1egrvtxdg1  29977  umgr2v2evd2  29995  vdegp1bi  30005  mptprop  33178  altgnsg  33597  cyc3genpmlem  33599  elrspunsn  33865  esplyfval1  34091  bj-prmoore  37873  ftc1anclem8  38457  kelac2  43914  pr2el1  44397  pr2eldif1  44402  fourierdlem54  46996  sge0pr  47230  imarnf1pr  48178  paireqne  48419  fmtnoprmfac2lem1  48477  grlimprclnbgr  48920  grlimprclnbgredg  48921  1hegrlfgr  49056  fucoppcffth  50345  termc2  50452  uobeqterm  50480  2arwcatlem4  50532  incat  50535