MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  erref Structured version   Visualization version   GIF version

Theorem erref 8669
Description: An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypotheses
Ref Expression
ersymb.1 (𝜑𝑅 Er 𝑋)
erref.2 (𝜑𝐴𝑋)
Assertion
Ref Expression
erref (𝜑𝐴𝑅𝐴)

Proof of Theorem erref
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 erref.2 . . . 4 (𝜑𝐴𝑋)
2 ersymb.1 . . . . 5 (𝜑𝑅 Er 𝑋)
3 erdm 8659 . . . . 5 (𝑅 Er 𝑋 → dom 𝑅 = 𝑋)
42, 3syl 17 . . . 4 (𝜑 → dom 𝑅 = 𝑋)
51, 4eleqtrrd 2841 . . 3 (𝜑𝐴 ∈ dom 𝑅)
6 eldmg 5855 . . . 4 (𝐴𝑋 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
71, 6syl 17 . . 3 (𝜑 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
85, 7mpbid 231 . 2 (𝜑 → ∃𝑥 𝐴𝑅𝑥)
92adantr 482 . . 3 ((𝜑𝐴𝑅𝑥) → 𝑅 Er 𝑋)
10 simpr 486 . . 3 ((𝜑𝐴𝑅𝑥) → 𝐴𝑅𝑥)
119, 10, 10ertr4d 8668 . 2 ((𝜑𝐴𝑅𝑥) → 𝐴𝑅𝐴)
128, 11exlimddv 1939 1 (𝜑𝐴𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107   class class class wbr 5106  dom cdm 5634   Er wer 8646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-er 8649
This theorem is referenced by:  iserd  8675  erth  8698  iiner  8729  erinxp  8731  nqerid  10870  enqeq  10871  qusgrp  18986  sylow2alem1  19400  sylow2alem2  19401  sylow2a  19402  efginvrel2  19510  efgsrel  19517  efgcpbllemb  19538  frgp0  19543  frgpnabllem1  19652  frgpnabllem2  19653  pcophtb  24395  pi1xfrf  24419  pi1xfr  24421  pi1xfrcnvlem  24422  ecref  31628  prtlem10  37330  prjspner01  40966  prjspner1  40967
  Copyright terms: Public domain W3C validator