Theorem prid1g 4699

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 2740	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 871	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4585	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 259	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  prid2g  4700  prid1  4701  prnzg  4717  preq1b  4784  prel12g  4802  elpreqprb  4806  prproe  4843  opth1  5422  fr2nr  5602  fpr2g  7162  f1prex  7235  fveqf1o  7253  fvf1pr  7258  pw2f1olem  9016  hashprdifel  14358  gcdcllem3  16468  mgm2nsgrplem1  18887  mgm2nsgrplem2  18888  mgm2nsgrplem3  18889  sgrp2nmndlem1  18892  sgrp2rid2  18895  pmtrprfv  19426  pptbas  22998  coseq0negpitopi  26492  uhgr2edg  29302  umgrvad2edg  29307  uspgr2v1e2w  29345  usgr2v1e2w  29346  nbusgredgeu0  29462  nbusgrf1o0  29463  nb3grprlem1  29474  nb3grprlem2  29475  vtxduhgr0nedg  29586  1hegrvtxdg1  29601  1egrvtxdg1  29603  umgr2v2evd2  29621  vdegp1bi  29631  mptprop  32797  altgnsg  33237  cyc3genpmlem  33239  elrspunsn  33519  esplyfval1  33764  bj-prmoore  37480  ftc1anclem8  38074  kelac2  43517  pr2el1  44000  pr2eldif1  44005  fourierdlem54  46610  sge0pr  46844  imarnf1pr  47752  paireqne  47993  fmtnoprmfac2lem1  48051  grlimprclnbgr  48494  grlimprclnbgredg  48495  1hegrlfgr  48630  fucoppcffth  49908  termc2  50015  uobeqterm  50043  2arwcatlem4  50095  incat  50098