Theorem ssdm ≪ | index | src | ≫ 

theorem ssdm (A R: set): $ Dom R C_ A <-> R C_ Xp A _V $;
StepHypRefExpression
1 bitr4 
(Dom R C_ A <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)) ->
  (R C_ Xp A _V <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)) ->
  (Dom R C_ A <-> R C_ Xp A _V)
2 bitr 
(a1 e. Dom R -> a1 e. A <-> E. a2 a1, a2 e. R -> a1 e. A) ->
  (E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)) ->
  (a1 e. Dom R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V))
3 eldm 
a1 e. Dom R <-> E. a2 a1, a2 e. R
4 3 imeq1i 
a1 e. Dom R -> a1 e. A <-> E. a2 a1, a2 e. R -> a1 e. A
5 2, 4 ax_mp 
(E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)) -> (a1 e. Dom R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V))
6 bitr4 
(E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1 e. A)) ->
  (A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V) <-> A. a2 (a1, a2 e. R -> a1 e. A)) ->
  (E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V))
7 eexb 
E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1 e. A)
8 6, 7 ax_mp 
(A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V) <-> A. a2 (a1, a2 e. R -> a1 e. A)) -> (E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V))
9 bitr 
(a1, a2 e. Xp A _V <-> a1 e. A /\ a2 e. _V) -> (a1 e. A /\ a2 e. _V <-> a1 e. A) -> (a1, a2 e. Xp A _V <-> a1 e. A)
10 prelxp 
a1, a2 e. Xp A _V <-> a1 e. A /\ a2 e. _V
11 9, 10 ax_mp 
(a1 e. A /\ a2 e. _V <-> a1 e. A) -> (a1, a2 e. Xp A _V <-> a1 e. A)
12 bian2 
a2 e. _V -> (a1 e. A /\ a2 e. _V <-> a1 e. A)
13 elv 
a2 e. _V
14 12, 13 ax_mp 
a1 e. A /\ a2 e. _V <-> a1 e. A
15 11, 14 ax_mp 
a1, a2 e. Xp A _V <-> a1 e. A
16 15 imeq2i 
a1, a2 e. R -> a1, a2 e. Xp A _V <-> a1, a2 e. R -> a1 e. A
17 16 aleqi 
A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V) <-> A. a2 (a1, a2 e. R -> a1 e. A)
18 8, 17 ax_mp 
E. a2 a1, a2 e. R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)
19 5, 18 ax_mp 
a1 e. Dom R -> a1 e. A <-> A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)
20 19 aleqi 
A. a1 (a1 e. Dom R -> a1 e. A) <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)
21 20 conv subset 
Dom R C_ A <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)
22 1, 21 ax_mp 
(R C_ Xp A _V <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)) -> (Dom R C_ A <-> R C_ Xp A _V)
23 ssal2 
R C_ Xp A _V <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp A _V)
24 22, 23 ax_mp 
Dom R C_ A <-> R C_ Xp A _V

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)