Theorem prid1g 4705

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  prid2g  4706  prid1  4707  prnzg  4723  preq1b  4790  prel12g  4808  elpreqprb  4812  prproe  4849  opth1  5421  fr2nr  5599  fpr2g  7157  f1prex  7230  fveqf1o  7248  fvf1pr  7253  pw2f1olem  9010  hashprdifel  14322  gcdcllem3  16429  mgm2nsgrplem1  18847  mgm2nsgrplem2  18848  mgm2nsgrplem3  18849  sgrp2nmndlem1  18852  sgrp2rid2  18855  pmtrprfv  19386  pptbas  22951  coseq0negpitopi  26452  uhgr2edg  29265  umgrvad2edg  29270  uspgr2v1e2w  29308  usgr2v1e2w  29309  nbusgredgeu0  29425  nbusgrf1o0  29426  nb3grprlem1  29437  nb3grprlem2  29438  vtxduhgr0nedg  29550  1hegrvtxdg1  29565  1egrvtxdg1  29567  umgr2v2evd2  29585  vdegp1bi  29595  mptprop  32760  altgnsg  33215  cyc3genpmlem  33217  elrspunsn  33494  esplyfval1  33722  bj-prmoore  37425  ftc1anclem8  38012  kelac2  43496  pr2el1  43979  pr2eldif1  43984  fourierdlem54  46592  sge0pr  46826  imarnf1pr  47716  paireqne  47945  fmtnoprmfac2lem1  48000  grlimprclnbgr  48430  grlimprclnbgredg  48431  1hegrlfgr  48566  fucoppcffth  49844  termc2  49951  uobeqterm  49979  2arwcatlem4  50031  incat  50034