Theorem all2all1 ≪ | index | src | ≫ 

theorem all2all1 (A: set) (l1 l2: nat) {x y: nat}:
  $ l1, l2 e. all2 (S\ x, {y | x e. A}) -> all A l1 $;
StepHypRefExpression
1 all2com 
l2, l1 e. all2 (cnv (S\ x, {y | x e. A})) <-> l1, l2 e. all2 (S\ x, {y | x e. A})
2 eleq2 
all2 (cnv (S\ x, {y | x e. A})) == all2 (S\ y, A) -> (l2, l1 e. all2 (cnv (S\ x, {y | x e. A})) <-> l2, l1 e. all2 (S\ y, A))
3 all2eq 
cnv (S\ x, {y | x e. A}) == S\ y, A -> all2 (cnv (S\ x, {y | x e. A})) == all2 (S\ y, A)
4 eqstr 
cnv (S\ x, {y | x e. A}) == S\ y, {x | x e. A} -> S\ y, {x | x e. A} == S\ y, A -> cnv (S\ x, {y | x e. A}) == S\ y, A
5 cnvopab 
cnv (S\ x, {y | x e. A}) == S\ y, {x | x e. A}
6 4, 5 ax_mp 
S\ y, {x | x e. A} == S\ y, A -> cnv (S\ x, {y | x e. A}) == S\ y, A
7 abid2 
{x | x e. A} == A
8 7 sabeqi 
S\ y, {x | x e. A} == S\ y, A
9 6, 8 ax_mp 
cnv (S\ x, {y | x e. A}) == S\ y, A
10 3, 9 ax_mp 
all2 (cnv (S\ x, {y | x e. A})) == all2 (S\ y, A)
11 2, 10 ax_mp 
l2, l1 e. all2 (cnv (S\ x, {y | x e. A})) <-> l2, l1 e. all2 (S\ y, A)
12 all2all2 
l2, l1 e. all2 (S\ y, A) -> all A l1
13 11, 12 sylbi 
l2, l1 e. all2 (cnv (S\ x, {y | x e. A})) -> all A l1
14 1, 13 sylbir 
l1, l2 e. all2 (S\ x, {y | x e. A}) -> all A l1

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)