Theorem rlamrnss ≪ | index | src | ≫ 

theorem rlamrnss (B: set) (a: nat) {x: nat} (b: nat x):
  $ Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. B) $;
StepHypRefExpression
1 bitr 
(Ran (\. x e. a, b) C_ B <-> (\ x, b) '' a C_ B) -> ((\ x, b) '' a C_ B <-> A. x (x e. a -> b e. B)) -> (Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. B))
2 sseq1 
Ran (\. x e. a, b) == (\ x, b) '' a -> (Ran (\. x e. a, b) C_ B <-> (\ x, b) '' a C_ B)
3 rnrlam 
Ran (\. x e. a, b) == (\ x, b) '' a
4 2, 3 ax_mp 
Ran (\. x e. a, b) C_ B <-> (\ x, b) '' a C_ B
5 1, 4 ax_mp 
((\ x, b) '' a C_ B <-> A. x (x e. a -> b e. B)) -> (Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. B))
6 bitr 
((\ x, b) '' a C_ B <-> A. y A. x (x e. a /\ y = b -> y e. B)) ->
  (A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B)) ->
  ((\ x, b) '' a C_ B <-> A. x (x e. a -> b e. B))
7 bitr 
(y e. (\ x, b) '' a -> y e. B <-> E. x (x e. a /\ y = b) -> y e. B) ->
  (E. x (x e. a /\ y = b) -> y e. B <-> A. x (x e. a /\ y = b -> y e. B)) ->
  (y e. (\ x, b) '' a -> y e. B <-> A. x (x e. a /\ y = b -> y e. B))
8 ellamima 
y e. (\ x, b) '' a <-> E. x (x e. a /\ y = b)
9 8 imeq1i 
y e. (\ x, b) '' a -> y e. B <-> E. x (x e. a /\ y = b) -> y e. B
10 7, 9 ax_mp 
(E. x (x e. a /\ y = b) -> y e. B <-> A. x (x e. a /\ y = b -> y e. B)) -> (y e. (\ x, b) '' a -> y e. B <-> A. x (x e. a /\ y = b -> y e. B))
11 eexb 
E. x (x e. a /\ y = b) -> y e. B <-> A. x (x e. a /\ y = b -> y e. B)
12 10, 11 ax_mp 
y e. (\ x, b) '' a -> y e. B <-> A. x (x e. a /\ y = b -> y e. B)
13 12 aleqi 
A. y (y e. (\ x, b) '' a -> y e. B) <-> A. y A. x (x e. a /\ y = b -> y e. B)
14 13 conv subset 
(\ x, b) '' a C_ B <-> A. y A. x (x e. a /\ y = b -> y e. B)
15 6, 14 ax_mp 
(A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B)) -> ((\ x, b) '' a C_ B <-> A. x (x e. a -> b e. B))
16 bitr 
(A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x A. y (x e. a /\ y = b -> y e. B)) ->
  (A. x A. y (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B)) ->
  (A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B))
17 alcomb 
A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x A. y (x e. a /\ y = b -> y e. B)
18 16, 17 ax_mp 
(A. x A. y (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B)) -> (A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B))
19 bitr 
(A. y (x e. a /\ y = b -> y e. B) <-> A. y (y = b -> x e. a -> y e. B)) ->
  (A. y (y = b -> x e. a -> y e. B) <-> x e. a -> b e. B) ->
  (A. y (x e. a /\ y = b -> y e. B) <-> x e. a -> b e. B)
20 bitr 
(x e. a /\ y = b -> y e. B <-> y = b /\ x e. a -> y e. B) ->
  (y = b /\ x e. a -> y e. B <-> y = b -> x e. a -> y e. B) ->
  (x e. a /\ y = b -> y e. B <-> y = b -> x e. a -> y e. B)
21 ancomb 
x e. a /\ y = b <-> y = b /\ x e. a
22 21 imeq1i 
x e. a /\ y = b -> y e. B <-> y = b /\ x e. a -> y e. B
23 20, 22 ax_mp 
(y = b /\ x e. a -> y e. B <-> y = b -> x e. a -> y e. B) -> (x e. a /\ y = b -> y e. B <-> y = b -> x e. a -> y e. B)
24 impexp 
y = b /\ x e. a -> y e. B <-> y = b -> x e. a -> y e. B
25 23, 24 ax_mp 
x e. a /\ y = b -> y e. B <-> y = b -> x e. a -> y e. B
26 25 aleqi 
A. y (x e. a /\ y = b -> y e. B) <-> A. y (y = b -> x e. a -> y e. B)
27 19, 26 ax_mp 
(A. y (y = b -> x e. a -> y e. B) <-> x e. a -> b e. B) -> (A. y (x e. a /\ y = b -> y e. B) <-> x e. a -> b e. B)
28 eleq1 
y = b -> (y e. B <-> b e. B)
29 28 imeq2d 
y = b -> (x e. a -> y e. B <-> x e. a -> b e. B)
30 29 aleqe 
A. y (y = b -> x e. a -> y e. B) <-> x e. a -> b e. B
31 27, 30 ax_mp 
A. y (x e. a /\ y = b -> y e. B) <-> x e. a -> b e. B
32 31 aleqi 
A. x A. y (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B)
33 18, 32 ax_mp 
A. y A. x (x e. a /\ y = b -> y e. B) <-> A. x (x e. a -> b e. B)
34 15, 33 ax_mp 
(\ x, b) '' a C_ B <-> A. x (x e. a -> b e. B)
35 5, 34 ax_mp 
Ran (\. x e. a, b) C_ B <-> A. x (x e. a -> b e. 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)