Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elprg Unicode version

Theorem elprg 4045
 Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.)
Assertion
Ref Expression
elprg

Proof of Theorem elprg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2461 . . 3
2 eqeq1 2461 . . 3
31, 2orbi12d 709 . 2
4 dfpr2 4044 . 2
53, 4elab2g 3248 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  \/wo 368  =wceq 1395  e.wcel 1818  {cpr 4031 This theorem is referenced by:  eldifpr  4046  elpr  4047  elpr2  4048  elpri  4049  eltpg  4071  ifpr  4077  prid1g  4136  ordunpr  6661  hashtpg  12523  cnsubrg  18478  atandm  23207  nbgra0nb  24429  eupath2lem1  24977  eliccioo  27627 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032
 Copyright terms: Public domain W3C validator