Theorem prid1g 4719

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

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

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 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  prid2g  4720  prid1  4721  prnzg  4737  preq1b  4804  prel12g  4822  elpreqprb  4826  prproe  4863  opth1  5431  fr2nr  5609  fpr2g  7167  f1prex  7240  fveqf1o  7258  fvf1pr  7263  pw2f1olem  9021  hashprdifel  14333  gcdcllem3  16440  mgm2nsgrplem1  18855  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  sgrp2nmndlem1  18860  sgrp2rid2  18863  pmtrprfv  19394  pptbas  22964  coseq0negpitopi  26480  uhgr2edg  29293  umgrvad2edg  29298  uspgr2v1e2w  29336  usgr2v1e2w  29337  nbusgredgeu0  29453  nbusgrf1o0  29454  nb3grprlem1  29465  nb3grprlem2  29466  vtxduhgr0nedg  29578  1hegrvtxdg1  29593  1egrvtxdg1  29595  umgr2v2evd2  29613  vdegp1bi  29623  mptprop  32787  altgnsg  33242  cyc3genpmlem  33244  elrspunsn  33521  esplyfval1  33749  bj-prmoore  37362  ftc1anclem8  37945  kelac2  43416  pr2el1  43899  pr2eldif1  43904  fourierdlem54  46512  sge0pr  46746  imarnf1pr  47636  paireqne  47865  fmtnoprmfac2lem1  47920  grlimprclnbgr  48350  grlimprclnbgredg  48351  1hegrlfgr  48486  fucoppcffth  49764  termc2  49871  uobeqterm  49899  2arwcatlem4  49951  incat  49954