Theorem elrn 5796

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 5794	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)

Syntax hints:   ↔ wb 205  ∃wex 1783   ∈ wcel 2107  Vcvv 3427   class class class wbr 5075  ran crn 5586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3071  df-v 3429  df-dif 3891  df-un 3893  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-br 5076  df-opab 5138  df-cnv 5593  df-dm 5595  df-rn 5596

This theorem is referenced by:  dmcosseq  5876  inisegn0  6000  rnco  6150  dffo4  6966  fvclss  7102  rntpos  8031  fpwwe2lem10  10343  fpwwe2lem11  10344  fclim  15206  perfdvf  25010  dftr6  33666  dffr5  33669  brsset  34160  dfon3  34163  brtxpsd  34165  dffix2  34176  elsingles  34189  dfrdg4  34222  undmrnresiss  41143