Theorem enref 8951

Description: Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)

Hypothesis

Ref	Expression
enref.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
enref	⊢ 𝐴 ≈ 𝐴

Proof of Theorem enref

Step	Hyp	Ref	Expression
1		enref.1	. 2 ⊢ 𝐴 ∈ V
2		enrefg 8950	. 2 ⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ≈ 𝐴

Syntax hints:   ∈ wcel 2132  Vcvv 3444   class class class wbr 5090   ≈ cen 8909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-en 8913

This theorem is referenced by:  ener  8967  en0ALT  8985  pwen  9107  karden  9839  mappwen  10054  nnadju  10140  infmap2  10159  ackbij1lem5  10165  axcc4dom  10384  domtriomlem  10385  cfpwsdom  10528  0tsk  10699  fzennn  13967  qnnen  16217  rpnnen  16231  rexpen  16232  lmisfree  21863  met2ndci  24551  lgseisenlem2  27406  poimirlem9  38066  poimirlem26  38083  1aryenef  49205  2aryenef  49216