Theorem cnvopab ≪ | index | src | ≫ 

theorem cnvopab {x y: nat} (p: wff x y):
  $ cnv (S\ x, {y | p}) == S\ y, {x | p} $;
StepHypRefExpression
1 bitr 
(a1, a2 e. cnv (S\ x, {y | p}) <-> a2, a1 e. S\ x, {y | p}) ->
  (a2, a1 e. S\ x, {y | p} <-> a1, a2 e. S\ y, {x | p}) ->
  (a1, a2 e. cnv (S\ x, {y | p}) <-> a1, a2 e. S\ y, {x | p})
2 prcnv 
a1, a2 e. cnv (S\ x, {y | p}) <-> a2, a1 e. S\ x, {y | p}
3 1, 2 ax_mp 
(a2, a1 e. S\ x, {y | p} <-> a1, a2 e. S\ y, {x | p}) -> (a1, a2 e. cnv (S\ x, {y | p}) <-> a1, a2 e. S\ y, {x | p})
4 bitr 
(a2, a1 e. S\ x, {y | p} <-> a1 e. S[a2 / x] {y | p}) ->
  (a1 e. S[a2 / x] {y | p} <-> a1, a2 e. S\ y, {x | p}) ->
  (a2, a1 e. S\ x, {y | p} <-> a1, a2 e. S\ y, {x | p})
5 elsabs 
a2, a1 e. S\ x, {y | p} <-> a1 e. S[a2 / x] {y | p}
6 4, 5 ax_mp 
(a1 e. S[a2 / x] {y | p} <-> a1, a2 e. S\ y, {x | p}) -> (a2, a1 e. S\ x, {y | p} <-> a1, a2 e. S\ y, {x | p})
7 bitr 
(a1 e. S[a2 / x] {y | p} <-> [a2 / x] a1 e. {y | p}) ->
  ([a2 / x] a1 e. {y | p} <-> a1, a2 e. S\ y, {x | p}) ->
  (a1 e. S[a2 / x] {y | p} <-> a1, a2 e. S\ y, {x | p})
8 elsbs 
a1 e. S[a2 / x] {y | p} <-> [a2 / x] a1 e. {y | p}
9 7, 8 ax_mp 
([a2 / x] a1 e. {y | p} <-> a1, a2 e. S\ y, {x | p}) -> (a1 e. S[a2 / x] {y | p} <-> a1, a2 e. S\ y, {x | p})
10 bitr4 
([a2 / x] a1 e. {y | p} <-> [a2 / x] [a1 / y] p) -> (a1, a2 e. S\ y, {x | p} <-> [a2 / x] [a1 / y] p) -> ([a2 / x] a1 e. {y | p} <-> a1, a2 e. S\ y, {x | p})
11 elab 
a1 e. {y | p} <-> [a1 / y] p
12 11 sbeq2i 
[a2 / x] a1 e. {y | p} <-> [a2 / x] [a1 / y] p
13 10, 12 ax_mp 
(a1, a2 e. S\ y, {x | p} <-> [a2 / x] [a1 / y] p) -> ([a2 / x] a1 e. {y | p} <-> a1, a2 e. S\ y, {x | p})
14 bitr 
(a1, a2 e. S\ y, {x | p} <-> a2 e. S[a1 / y] {x | p}) -> (a2 e. S[a1 / y] {x | p} <-> [a2 / x] [a1 / y] p) -> (a1, a2 e. S\ y, {x | p} <-> [a2 / x] [a1 / y] p)
15 elsabs 
a1, a2 e. S\ y, {x | p} <-> a2 e. S[a1 / y] {x | p}
16 14, 15 ax_mp 
(a2 e. S[a1 / y] {x | p} <-> [a2 / x] [a1 / y] p) -> (a1, a2 e. S\ y, {x | p} <-> [a2 / x] [a1 / y] p)
17 bitr 
(a2 e. S[a1 / y] {x | p} <-> [a1 / y] a2 e. {x | p}) -> ([a1 / y] a2 e. {x | p} <-> [a2 / x] [a1 / y] p) -> (a2 e. S[a1 / y] {x | p} <-> [a2 / x] [a1 / y] p)
18 elsbs 
a2 e. S[a1 / y] {x | p} <-> [a1 / y] a2 e. {x | p}
19 17, 18 ax_mp 
([a1 / y] a2 e. {x | p} <-> [a2 / x] [a1 / y] p) -> (a2 e. S[a1 / y] {x | p} <-> [a2 / x] [a1 / y] p)
20 bitr4 
([a1 / y] a2 e. {x | p} <-> [a1 / y] [a2 / x] p) -> ([a2 / x] [a1 / y] p <-> [a1 / y] [a2 / x] p) -> ([a1 / y] a2 e. {x | p} <-> [a2 / x] [a1 / y] p)
21 elab 
a2 e. {x | p} <-> [a2 / x] p
22 21 sbeq2i 
[a1 / y] a2 e. {x | p} <-> [a1 / y] [a2 / x] p
23 20, 22 ax_mp 
([a2 / x] [a1 / y] p <-> [a1 / y] [a2 / x] p) -> ([a1 / y] a2 e. {x | p} <-> [a2 / x] [a1 / y] p)
24 sbcom 
[a2 / x] [a1 / y] p <-> [a1 / y] [a2 / x] p
25 23, 24 ax_mp 
[a1 / y] a2 e. {x | p} <-> [a2 / x] [a1 / y] p
26 19, 25 ax_mp 
a2 e. S[a1 / y] {x | p} <-> [a2 / x] [a1 / y] p
27 16, 26 ax_mp 
a1, a2 e. S\ y, {x | p} <-> [a2 / x] [a1 / y] p
28 13, 27 ax_mp 
[a2 / x] a1 e. {y | p} <-> a1, a2 e. S\ y, {x | p}
29 9, 28 ax_mp 
a1 e. S[a2 / x] {y | p} <-> a1, a2 e. S\ y, {x | p}
30 6, 29 ax_mp 
a2, a1 e. S\ x, {y | p} <-> a1, a2 e. S\ y, {x | p}
31 3, 30 ax_mp 
a1, a2 e. cnv (S\ x, {y | p}) <-> a1, a2 e. S\ y, {x | p}
32 31 eqri2 
cnv (S\ x, {y | p}) == S\ y, {x | p}

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)