Theorem dfex2_2 ≪ | index | src | ≫ 

theorem dfex2_2 (R: set) (l1 l2: nat):
  $ l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R) $;
StepHypRefExpression
1 bitr3 
(len l1 = len l2 /\ l1, l2 e. ex2 R <-> l1, l2 e. ex2 R) ->
  (len l1 = len l2 /\ l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R)) ->
  (l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R))
2 bian1a 
(l1, l2 e. ex2 R -> len l1 = len l2) -> (len l1 = len l2 /\ l1, l2 e. ex2 R <-> l1, l2 e. ex2 R)
3 ex2len 
l1, l2 e. ex2 R -> len l1 = len l2
4 2, 3 ax_mp 
len l1 = len l2 /\ l1, l2 e. ex2 R <-> l1, l2 e. ex2 R
5 1, 4 ax_mp 
(len l1 = len l2 /\ l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R)) -> (l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R))
6 aneq2a 
(len l1 = len l2 -> (l1, l2 e. ex2 R <-> ~l1, l2 e. all2 (Compl R))) -> (len l1 = len l2 /\ l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R))
7 con2b 
(l1, l2 e. all2 (Compl R) <-> ~l1, l2 e. ex2 R) -> (l1, l2 e. ex2 R <-> ~l1, l2 e. all2 (Compl R))
8 all2nex 
l1, l2 e. all2 (Compl R) <-> len l1 = len l2 /\ ~l1, l2 e. ex2 R
9 bian1 
len l1 = len l2 -> (len l1 = len l2 /\ ~l1, l2 e. ex2 R <-> ~l1, l2 e. ex2 R)
10 8, 9 syl5bb 
len l1 = len l2 -> (l1, l2 e. all2 (Compl R) <-> ~l1, l2 e. ex2 R)
11 7, 10 syl 
len l1 = len l2 -> (l1, l2 e. ex2 R <-> ~l1, l2 e. all2 (Compl R))
12 6, 11 ax_mp 
len l1 = len l2 /\ l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R)
13 5, 12 ax_mp 
l1, l2 e. ex2 R <-> len l1 = len l2 /\ ~l1, l2 e. all2 (Compl R)

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)