Theorem enref 9013

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 9012	. 2 ⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ≈ 𝐴

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102   ≈ cen 8971

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-en 8975

This theorem is used by:  ener  9029  en0ALT  9047  pwen  9170  karden  9960  kardenOLD  9961  mappwen  10192  nnadju  10277  infmap2  10296  ackbij1lem5  10302  axcc4dom  10520  domtriomlem  10521  cfpwsdom  10670  0tsk  10841  fzennn  14112  qnnen  16382  rpnnen  16396  rexpen  16397  lmisfree  22149  met2ndci  24842  lgseisenlem2  27704  poimirlem9  38623  poimirlem26  38640  1aryenef  49833  2aryenef  49844