Theorem imv ≪ | index | src | ≫ 

theorem imv (F: set): $ F '' _V == Ran F $;
StepHypRefExpression
1 bitr4 
(x e. F '' _V <-> E. y (y e. _V /\ y, x e. F)) -> (x e. Ran F <-> E. y (y e. _V /\ y, x e. F)) -> (x e. F '' _V <-> x e. Ran F)
2 elima 
x e. F '' _V <-> E. y (y e. _V /\ y, x e. F)
3 1, 2 ax_mp 
(x e. Ran F <-> E. y (y e. _V /\ y, x e. F)) -> (x e. F '' _V <-> x e. Ran F)
4 bitr4 
(x e. Ran F <-> E. y y, x e. F) -> (E. y (y e. _V /\ y, x e. F) <-> E. y y, x e. F) -> (x e. Ran F <-> E. y (y e. _V /\ y, x e. F))
5 elrn 
x e. Ran F <-> E. y y, x e. F
6 4, 5 ax_mp 
(E. y (y e. _V /\ y, x e. F) <-> E. y y, x e. F) -> (x e. Ran F <-> E. y (y e. _V /\ y, x e. F))
7 bian1 
y e. _V -> (y e. _V /\ y, x e. F <-> y, x e. F)
8 elv 
y e. _V
9 7, 8 ax_mp 
y e. _V /\ y, x e. F <-> y, x e. F
10 9 exeqi 
E. y (y e. _V /\ y, x e. F) <-> E. y y, x e. F
11 6, 10 ax_mp 
x e. Ran F <-> E. y (y e. _V /\ y, x e. F)
12 3, 11 ax_mp 
x e. F '' _V <-> x e. Ran F
13 12 eqri 
F '' _V == Ran F

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano2, addeq, muleq)