Theorem prid1g 4727

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  prid2g  4728  prid1  4729  prnzg  4745  preq1b  4812  prel12g  4830  elpreqprb  4834  prproe  4871  opth1  5459  fr2nr  5640  fpr2g  7211  f1prex  7284  fveqf1o  7302  fvf1pr  7307  pw2f1olem  9070  hashprdifel  14436  gcdcllem3  16560  mgm2nsgrplem1  18981  mgm2nsgrplem2  18982  mgm2nsgrplem3  18983  sgrp2nmndlem1  18986  sgrp2rid2  18989  pmtrprfv  19524  pptbas  23146  coseq0negpitopi  26649  uhgr2edg  29539  umgrvad2edg  29544  uspgr2v1e2w  29582  usgr2v1e2w  29583  nbusgredgeu0  29699  nbusgrf1o0  29700  nb3grprlem1  29711  nb3grprlem2  29712  vtxduhgr0nedg  29823  1hegrvtxdg1  29838  1egrvtxdg1  29840  umgr2v2evd2  29858  vdegp1bi  29868  mptprop  33024  altgnsg  33450  cyc3genpmlem  33452  elrspunsn  33718  esplyfval1  33944  bj-prmoore  37738  ftc1anclem8  38332  kelac2  43775  pr2el1  44258  pr2eldif1  44263  fourierdlem54  46857  sge0pr  47091  imarnf1pr  48002  paireqne  48243  fmtnoprmfac2lem1  48301  grlimprclnbgr  48744  grlimprclnbgredg  48745  1hegrlfgr  48880  fucoppcffth  50172  termc2  50279  uobeqterm  50307  2arwcatlem4  50359  incat  50362