Theorem eqsrlam ≪ | index | src | ≫ 

theorem eqsrlam (F: set) (a: nat) {x: nat} (b: nat x):
  $ F == \. x e. a, b <-> isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b) $;
StepHypRefExpression
1 bitr2 
(isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b) <-> isfun F /\ Dom F == a /\ F == \. x e. a, b) ->
  (isfun F /\ Dom F == a /\ F == \. x e. a, b <-> F == \. x e. a, b) ->
  (F == \. x e. a, b <-> isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b))
2 aneq2a 
(isfun F /\ Dom F == a -> (A. x (x e. a -> F @ x = b) <-> F == \. x e. a, b)) ->
  (isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b) <-> isfun F /\ Dom F == a /\ F == \. x e. a, b)
3 rlamapp 
\. x e. a, F @ x == F <-> isfun F /\ Dom F == a
4 rlameq2b 
\. x e. a, F @ x = \. x e. a, b <-> A. x (x e. a -> F @ x = b)
5 nsinj 
\. x e. a, F @ x == \. x e. a, b <-> \. x e. a, F @ x = \. x e. a, b
6 eqseq1 
\. x e. a, F @ x == F -> (\. x e. a, F @ x == \. x e. a, b <-> F == \. x e. a, b)
7 5, 6 syl5bbr 
\. x e. a, F @ x == F -> (\. x e. a, F @ x = \. x e. a, b <-> F == \. x e. a, b)
8 4, 7 syl5bbr 
\. x e. a, F @ x == F -> (A. x (x e. a -> F @ x = b) <-> F == \. x e. a, b)
9 3, 8 sylbir 
isfun F /\ Dom F == a -> (A. x (x e. a -> F @ x = b) <-> F == \. x e. a, b)
10 2, 9 ax_mp 
isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b) <-> isfun F /\ Dom F == a /\ F == \. x e. a, b
11 1, 10 ax_mp 
(isfun F /\ Dom F == a /\ F == \. x e. a, b <-> F == \. x e. a, b) -> (F == \. x e. a, b <-> isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b))
12 bian1a 
(F == \. x e. a, b -> isfun F /\ Dom F == a) -> (isfun F /\ Dom F == a /\ F == \. x e. a, b <-> F == \. x e. a, b)
13 rlamisf 
isfun (\. x e. a, b)
14 isfeq 
F == \. x e. a, b -> (isfun F <-> isfun (\. x e. a, b))
15 13, 14 mpbiri 
F == \. x e. a, b -> isfun F
16 dmrlam 
Dom (\. x e. a, b) == a
17 dmeq 
F == \. x e. a, b -> Dom F == Dom (\. x e. a, b)
18 16, 17 syl6eqs 
F == \. x e. a, b -> Dom F == a
19 15, 18 iand 
F == \. x e. a, b -> isfun F /\ Dom F == a
20 12, 19 ax_mp 
isfun F /\ Dom F == a /\ F == \. x e. a, b <-> F == \. x e. a, b
21 11, 20 ax_mp 
F == \. x e. a, b <-> isfun F /\ Dom F == a /\ A. x (x e. a -> F @ x = b)

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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)