Theorem prid1g 4714

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

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

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 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  prid2g  4715  prid1  4716  prnzg  4732  preq1b  4800  prel12g  4818  elpreqprb  4822  prproe  4859  opth1  5422  fr2nr  5600  fpr2g  7151  f1prex  7225  fveqf1o  7243  fvf1pr  7248  pw2f1olem  9005  hashprdifel  14323  gcdcllem3  16430  mgm2nsgrplem1  18810  mgm2nsgrplem2  18811  mgm2nsgrplem3  18812  sgrp2nmndlem1  18815  sgrp2rid2  18818  pmtrprfv  19350  pptbas  22911  coseq0negpitopi  26428  uhgr2edg  29171  umgrvad2edg  29176  uspgr2v1e2w  29214  usgr2v1e2w  29215  nbusgredgeu0  29331  nbusgrf1o0  29332  nb3grprlem1  29343  nb3grprlem2  29344  vtxduhgr0nedg  29456  1hegrvtxdg1  29471  1egrvtxdg1  29473  umgr2v2evd2  29491  vdegp1bi  29501  mptprop  32654  altgnsg  33104  cyc3genpmlem  33106  elrspunsn  33376  bj-prmoore  37088  ftc1anclem8  37679  kelac2  43038  pr2el1  43522  pr2eldif1  43527  fourierdlem54  46142  sge0pr  46376  imarnf1pr  47267  paireqne  47496  fmtnoprmfac2lem1  47551  grlimprclnbgr  47981  grlimprclnbgredg  47982  1hegrlfgr  48117  fucoppcffth  49397  termc2  49504  uobeqterm  49532  2arwcatlem4  49584  incat  49587