Theorem elrn 5876

Description: Membership in a range. (Contributed by NM, 2-Apr-2004.)

Hypothesis

Ref	Expression
elrn.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
elrn	⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elrn

Step	Hyp	Ref	Expression
1		elrn.1	. 2 ⊢ 𝐴 ∈ V
2		elrng 5874	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1811   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102  ran crn 5652

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-pr 5391

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-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  dmcosseq  5961  dmcosseqOLD  5962  inisegn0  6098  rnco  6256  rncoOLD  6257  dffo4  7108  fvclss  7249  rntpos  8264  fpwwe2lem10  10732  fpwwe2lem11  10733  fclim  15729  perfdvf  26232  dftr6  36640  dffr5  36643  brsset  36775  dfon3  36778  brtxpsd  36780  dffix2  36791  elsingles  36804  dfrdg4  36839  undmrnresiss  44741  cocanss2  46058