Theorem sabssxpe ≪ | index | src | ≫ 

theorem sabssxpe (A C: set) (a: nat) {x: nat} (B: set x):
  $ x = fst a -> snd a e. B -> x e. A /\ snd a e. C $ >
  $ a e. S\ x, B -> a e. Xp A C $;
StepHypRefExpression
1 anr 
T. /\ a e. Xp A C -> a e. Xp A C
2 anim1 
(x e. A -> T. /\ x e. A) -> x e. A /\ snd a e. C -> T. /\ x e. A /\ snd a e. C
3 ian 
T. -> x e. A -> T. /\ x e. A
4 3 trud 
x e. A -> T. /\ x e. A
5 2, 4 ax_mp 
x e. A /\ snd a e. C -> T. /\ x e. A /\ snd a e. C
6 hyp h 
x = fst a -> snd a e. B -> x e. A /\ snd a e. C
7 5, 6 syl6 
x = fst a -> snd a e. B -> T. /\ x e. A /\ snd a e. C
8 7 anwr 
T. /\ x = fst a -> snd a e. B -> T. /\ x e. A /\ snd a e. C
9 8 sabssxped 
T. -> a e. S\ x, B -> T. /\ a e. Xp A C
10 1, 9 syl6 
T. -> a e. S\ x, B -> a e. Xp A C
11 10 trud 
a e. S\ x, B -> a e. Xp A C

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)