Theorem erref 8655

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 8645	. . . . 5 ⊢ (𝑅 Er 𝑋 → dom 𝑅 = 𝑋)
4	2, 3	syl 17	. . . 4 ⊢ (𝜑 → dom 𝑅 = 𝑋)
5	1, 4	eleqtrrd 2839	. . 3 ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)
6		eldmg 5847	. . . 4 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
7	1, 6	syl 17	. . 3 ⊢ (𝜑 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
8	5, 7	mpbid 232	. 2 ⊢ (𝜑 → ∃𝑥 𝐴𝑅𝑥)
9	2	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐴𝑅𝑥) → 𝑅 Er 𝑋)
10		simpr 484	. . 3 ⊢ ((𝜑 ∧ 𝐴𝑅𝑥) → 𝐴𝑅𝑥)
11	9, 10, 10	ertr4d 8654	. 2 ⊢ ((𝜑 ∧ 𝐴𝑅𝑥) → 𝐴𝑅𝐴)
12	8, 11	exlimddv 1936	1 ⊢ (𝜑 → 𝐴𝑅𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113   class class class wbr 5098  dom cdm 5624   Er wer 8632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-er 8635

This theorem is referenced by:  iserd  8661  ecref  8680  erth  8689  iiner  8726  erinxp  8728  nqerid  10844  enqeq  10845  qusgrp  19115  sylow2alem1  19546  sylow2alem2  19547  sylow2a  19548  efginvrel2  19656  efgsrel  19663  efgcpbllemb  19684  frgp0  19689  frgpnabllem1  19802  frgpnabllem2  19803  pcophtb  24985  pi1xfrf  25009  pi1xfr  25011  pi1xfrcnvlem  25012  prtlem10  39121  prjspner01  42864  prjspner1  42865  chnerlem1  47122  chner  47125