Theorem erref 8723

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.

Step	Hyp	Ref	Expression
1		erref.2	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
2		ersymb.1	. . . . 5 ⊢ (𝜑 → 𝑅 Er 𝑋)
3		erdm 8713	. . . . 5 ⊢ (𝑅 Er 𝑋 → dom 𝑅 = 𝑋)
4	2, 3	syl 17	. . . 4 ⊢ (𝜑 → dom 𝑅 = 𝑋)
5	1, 4	eleqtrrd 2837	. . 3 ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)
6		eldmg 5899	. . . 4 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
7	1, 6	syl 17	. . 3 ⊢ (𝜑 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
8	5, 7	mpbid 231	. 2 ⊢ (𝜑 → ∃𝑥 𝐴𝑅𝑥)
9	2	adantr 482	. . 3 ⊢ ((𝜑 ∧ 𝐴𝑅𝑥) → 𝑅 Er 𝑋)
10		simpr 486	. . 3 ⊢ ((𝜑 ∧ 𝐴𝑅𝑥) → 𝐴𝑅𝑥)
11	9, 10, 10	ertr4d 8722	. 2 ⊢ ((𝜑 ∧ 𝐴𝑅𝑥) → 𝐴𝑅𝐴)
12	8, 11	exlimddv 1939	1 ⊢ (𝜑 → 𝐴𝑅𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107   class class class wbr 5149  dom cdm 5677   Er wer 8700

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

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 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-er 8703

This theorem is referenced by:  iserd  8729  erth  8752  iiner  8783  erinxp  8785  nqerid  10928  enqeq  10929  qusgrp  19065  sylow2alem1  19485  sylow2alem2  19486  sylow2a  19487  efginvrel2  19595  efgsrel  19602  efgcpbllemb  19623  frgp0  19628  frgpnabllem1  19741  frgpnabllem2  19742  pcophtb  24545  pi1xfrf  24569  pi1xfr  24571  pi1xfrcnvlem  24572  ecref  31933  prtlem10  37735  prjspner01  41367  prjspner1  41368