Theorem fvex 5340

Description: The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by set.mm contributors, 30-Dec-1996.)

Assertion

Ref	Expression
fvex	⊢ (F ‘A) ∈ V

Proof of Theorem fvex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 4796	. 2 ⊢ (F ‘A) = (℩xAFx)
2		iotaex 4357	. 2 ⊢ (℩xAFx) ∈ V
3	1, 2	eqeltri 2423	1 ⊢ (F ‘A) ∈ V

Syntax hints:   ∈ wcel 1710  Vcvv 2860  ℩cio 4338   class class class wbr 4640   ‘cfv 4782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-sn 3742  df-pr 3743  df-uni 3893  df-iota 4340  df-fv 4796

This theorem is referenced by:  dffn5  5364  fvelrnb  5366  funimass4  5369  fvelimab  5371  fniinfv  5373  funfv  5376  dmfco  5382  fvimacnvi  5403  fvimacnv  5404  funconstss  5407  fsn2  5435  fnressn  5439  fniunfv  5467  funiunfv  5468  dff13  5472  isomin  5497  f1oiso  5500  ovex  5552  fvmptex  5722  fvmptnf  5724  txpcofun  5804  enprmaplem3  6079  nenpw1pwlem1  6085  1cnc  6140  nchoicelem6  6295  nchoicelem7  6296  nchoicelem12  6301  nchoicelem13  6302  nchoicelem14  6303  nchoicelem17  6306