Theorem isfrnss ≪ | index | src | ≫ 

theorem isfrnss (A F: set) {x: nat}:
  $ isfun F -> (Ran F C_ A <-> A. x (x e. Dom F -> F @ x e. A)) $;
StepHypRefExpression
1 bitr 
(A. a1 (F @ x = a1 -> a1 e. A) <-> A. a1 (a1 = F @ x -> a1 e. A)) ->
  (A. a1 (a1 = F @ x -> a1 e. A) <-> F @ x e. A) ->
  (A. a1 (F @ x = a1 -> a1 e. A) <-> F @ x e. A)
2 eqcomb 
F @ x = a1 <-> a1 = F @ x
3 2 imeq1i 
F @ x = a1 -> a1 e. A <-> a1 = F @ x -> a1 e. A
4 3 aleqi 
A. a1 (F @ x = a1 -> a1 e. A) <-> A. a1 (a1 = F @ x -> a1 e. A)
5 1, 4 ax_mp 
(A. a1 (a1 = F @ x -> a1 e. A) <-> F @ x e. A) -> (A. a1 (F @ x = a1 -> a1 e. A) <-> F @ x e. A)
6 eleq1 
a1 = F @ x -> (a1 e. A <-> F @ x e. A)
7 6 aleqe 
A. a1 (a1 = F @ x -> a1 e. A) <-> F @ x e. A
8 5, 7 ax_mp 
A. a1 (F @ x = a1 -> a1 e. A) <-> F @ x e. A
9 8 imeq2i 
x e. Dom F -> A. a1 (F @ x = a1 -> a1 e. A) <-> x e. Dom F -> F @ x e. A
10 9 aleqi 
A. x (x e. Dom F -> A. a1 (F @ x = a1 -> a1 e. A)) <-> A. x (x e. Dom F -> F @ x e. A)
11 ralalcomb 
A. x (x e. Dom F -> A. a1 (F @ x = a1 -> a1 e. A)) <-> A. a1 A. x (x e. Dom F -> F @ x = a1 -> a1 e. A)
12 erexb 
E. x (x e. Dom F /\ F @ x = a1) -> a1 e. A <-> A. x (x e. Dom F -> F @ x = a1 -> a1 e. A)
13 isfrn 
isfun F -> (a1 e. Ran F <-> E. x (x e. Dom F /\ F @ x = a1))
14 13 imeq1d 
isfun F -> (a1 e. Ran F -> a1 e. A <-> E. x (x e. Dom F /\ F @ x = a1) -> a1 e. A)
15 12, 14 syl6bb 
isfun F -> (a1 e. Ran F -> a1 e. A <-> A. x (x e. Dom F -> F @ x = a1 -> a1 e. A))
16 15 aleqd 
isfun F -> (A. a1 (a1 e. Ran F -> a1 e. A) <-> A. a1 A. x (x e. Dom F -> F @ x = a1 -> a1 e. A))
17 16 conv subset 
isfun F -> (Ran F C_ A <-> A. a1 A. x (x e. Dom F -> F @ x = a1 -> a1 e. A))
18 11, 17 syl6bbr 
isfun F -> (Ran F C_ A <-> A. x (x e. Dom F -> A. a1 (F @ x = a1 -> a1 e. A)))
19 10, 18 syl6bb 
isfun F -> (Ran F C_ A <-> A. x (x e. Dom F -> F @ x e. A))

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)