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  5423  fr2nr  5601  fpr2g  7159  f1prex  7232  fveqf1o  7250  fvf1pr  7255  pw2f1olem  9012  hashprdifel  14351  gcdcllem3  16461  mgm2nsgrplem1  18880  mgm2nsgrplem2  18881  mgm2nsgrplem3  18882  sgrp2nmndlem1  18885  sgrp2rid2  18888  pmtrprfv  19419  pptbas  22983  coseq0negpitopi  26480  uhgr2edg  29291  umgrvad2edg  29296  uspgr2v1e2w  29334  usgr2v1e2w  29335  nbusgredgeu0  29451  nbusgrf1o0  29452  nb3grprlem1  29463  nb3grprlem2  29464  vtxduhgr0nedg  29576  1hegrvtxdg1  29591  1egrvtxdg1  29593  umgr2v2evd2  29611  vdegp1bi  29621  mptprop  32786  altgnsg  33225  cyc3genpmlem  33227  elrspunsn  33504  esplyfval1  33732  bj-prmoore  37443  ftc1anclem8  38035  kelac2  43511  pr2el1  43994  pr2eldif1  43999  fourierdlem54  46606  sge0pr  46840  imarnf1pr  47742  paireqne  47983  fmtnoprmfac2lem1  48041  grlimprclnbgr  48484  grlimprclnbgredg  48485  1hegrlfgr  48620  fucoppcffth  49898  termc2  50005  uobeqterm  50033  2arwcatlem4  50085  incat  50088