| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1757 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1102 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (311 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (161 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (121 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Global Index
A
anything_in_next_of_itself [lemma, in FunctionsInZFC.Functions_in_ZFC]anything_sub_next_of_itself [lemma, in FunctionsInZFC.Functions_in_ZFC]
A_in_next_A_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
A_in_next_A_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
A_in_next_A_proof.N [variable, in FunctionsInZFC.Functions_in_ZFC]
A_in_next_A_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
A_in_next_A_proof [section, in FunctionsInZFC.Functions_in_ZFC]
A_sub_next_A_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
A_sub_next_A_proof.N [variable, in FunctionsInZFC.Functions_in_ZFC]
A_sub_next_A_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
A_sub_next_A_proof [section, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair [lemma, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.M [variable, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof [section, in FunctionsInZFC.Functions_in_ZFC]
A_sub_V_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
A_sub_V_proof1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
B
Big_Extensionality [lemma, in FunctionsInZFC.Functions_in_ZFC]big_extensionality_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.iYS [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.iXS [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.S [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.eYX [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.iYD [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.iXD [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded [definition, in FunctionsInZFC.Functions_in_ZFC]
boundedsubprops1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_pre [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof2_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.Bounded_NN_proof2.w [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.Bounded_NN_proof2.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.Bounded_NN_proof2 [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.v [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.u [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_sub2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.b [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.s [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.Q [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.P [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2 [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1.k [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1 [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.s [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.Q [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.P [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1 [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded_CHOICE_pr [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_CHOICE [definition, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Bounded_By [definition, in FunctionsInZFC.Functions_in_ZFC]
B_sub_V_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
B_sub_V_proof1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
b_in_Union_a [definition, in FunctionsInZFC.Functions_in_ZFC]
C
Cartesian [definition, in FunctionsInZFC.Functions_in_ZFC]cartesian_subs_are_relations [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pair_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pair_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_proj2_th [lemma, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_proj1_th [lemma, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_construction [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.Y1 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.X1 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.U [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.j [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.i [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.X [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.B [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.A [variable, in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section [section, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartpair [section, in FunctionsInZFC.Functions_in_ZFC]
cartpairA_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartpairB_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
cartpair.A [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.B [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.i [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.U [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.X [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.X1 [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
cartpair.Y1 [variable, in FunctionsInZFC.Functions_in_ZFC]
CHOICE [axiom, in FunctionsInZFC.Functions_in_ZFC]
CHOICE_pr [axiom, in FunctionsInZFC.Functions_in_ZFC]
Choose_an_element_pr [lemma, in FunctionsInZFC.Functions_in_ZFC]
Choose_an_element [definition, in FunctionsInZFC.Functions_in_ZFC]
COMP [definition, in FunctionsInZFC.Functions_in_ZFC]
composition_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
composition_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
composition_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
composition_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
composition_well_definedness [lemma, in FunctionsInZFC.Functions_in_ZFC]
composition_bounded [lemma, in FunctionsInZFC.Functions_in_ZFC]
composition_bounded_by [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMPp [section, in FunctionsInZFC.Functions_in_ZFC]
COMPp_Out4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMPp_Out3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMPp.F [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.G [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.i [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.X [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
COMPp.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
COMP_assoc [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_assoc_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step10 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.W [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.p [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.P [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.H [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2 [section, in FunctionsInZFC.Functions_in_ZFC]
COMP_assoc_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step10 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.W [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.p [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.P [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.H [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1 [section, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.W [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.j [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.i [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.g [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.f [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3 [section, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.j [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.i [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2 [section, in FunctionsInZFC.Functions_in_ZFC]
COMP_th5 [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.W [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.j [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1 [section, in FunctionsInZFC.Functions_in_ZFC]
comp_wd_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.W [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.V [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.j [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.i [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.g [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.f [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_wd [section, in FunctionsInZFC.Functions_in_ZFC]
COMP_th4p [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_th3p [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_INTERp [definition, in FunctionsInZFC.Functions_in_ZFC]
COMP_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
COMP_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_prop_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.c [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.X [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.G [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.F [variable, in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3 [section, in FunctionsInZFC.Functions_in_ZFC]
Comp_prop_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_prop_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER [definition, in FunctionsInZFC.Functions_in_ZFC]
Comp_intern [projection, in FunctionsInZFC.Functions_in_ZFC]
Comp_pair [projection, in FunctionsInZFC.Functions_in_ZFC]
Comp_prop [record, in FunctionsInZFC.Functions_in_ZFC]
Comp_inter_yz [projection, in FunctionsInZFC.Functions_in_ZFC]
Comp_inter_xy [projection, in FunctionsInZFC.Functions_in_ZFC]
Comp_inter [record, in FunctionsInZFC.Functions_in_ZFC]
Contains_NN_Naturals [lemma, in FunctionsInZFC.Functions_in_ZFC]
Contains_NN_nexts [projection, in FunctionsInZFC.Functions_in_ZFC]
Contains_NN_zero [projection, in FunctionsInZFC.Functions_in_ZFC]
Contains_NN [record, in FunctionsInZFC.Functions_in_ZFC]
counting_lem2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
counting_lem1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
covering_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
covering_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
covering_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
covering_em_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step13 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step12 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB5 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB4 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB3 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB2 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB1 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.iB [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B [section, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step11 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA5 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA4 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA3 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA2 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA1 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.iA [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A [section, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step10 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.GB [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.GA [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.FB [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.FA [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.contra [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em [section, in FunctionsInZFC.Functions_in_ZFC]
covering_1.iX [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.step0a [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.U [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.jx [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.ix [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.j [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.v [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.u [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.g [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.f [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.G [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.B [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
covering_1 [section, in FunctionsInZFC.Functions_in_ZFC]
cpb1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
D
distinct_Doubletons_have_geq_2_elements [lemma, in FunctionsInZFC.Functions_in_ZFC]distinct_doubletons_have_geq_2_elements_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.iYD [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.iXD [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.n [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof [section, in FunctionsInZFC.Functions_in_ZFC]
DOESNT_EXIST [definition, in FunctionsInZFC.Functions_in_ZFC]
Domain [definition, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Domain_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.p [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1 [section, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.T [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Domain_prop [definition, in FunctionsInZFC.Functions_in_ZFC]
Doubleton [definition, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_uniqueness [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.conclusionBD [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.conclusionAC [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_2_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2.step1_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2.k [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2 [section, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_1.step1_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_1.k [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_1 [section, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iBdoub [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iAdoub [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iB [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iA [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.Doub [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.nD [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.pC [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.nB [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.pA [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.C [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th4_b [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.n [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th4_a [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_sub2_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2.step2_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2.step2_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2.u [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2 [section, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_sub1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1.step1_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1.u [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1 [section, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.sY [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.sX [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.n [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.sYsubA [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.sXsubA [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.iYA [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.iXA [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.iYsY [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.iXsX [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
E
ee_eq_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]ee_eq_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.d [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.g [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.f [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.G [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof [section, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step12 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step11 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step10a [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step10 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.W [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.V [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.M [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.s [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.g [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.f [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.G [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof [section, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.j [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.G [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof [section, in FunctionsInZFC.Functions_in_ZFC]
efdom [section, in FunctionsInZFC.Functions_in_ZFC]
efdom_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
efdom.i [variable, in FunctionsInZFC.Functions_in_ZFC]
efdom.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
efdom.X [variable, in FunctionsInZFC.Functions_in_ZFC]
efdom.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
Element_of_NN [definition, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.i [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2 [section, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1 [section, in FunctionsInZFC.Functions_in_ZFC]
emptyfn1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
emptyfn2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
EmptySet [axiom, in FunctionsInZFC.Functions_in_ZFC]
EmptySet_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything_2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2.h [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2.B [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2 [section, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.A [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything [section, in FunctionsInZFC.Functions_in_ZFC]
EmptySet_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty.h [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty.X [variable, in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty [section, in FunctionsInZFC.Functions_in_ZFC]
EmptySet_pr [axiom, in FunctionsInZFC.Functions_in_ZFC]
empty_function_domain [lemma, in FunctionsInZFC.Functions_in_ZFC]
empty_function_domain_empty [lemma, in FunctionsInZFC.Functions_in_ZFC]
empty_function_function [lemma, in FunctionsInZFC.Functions_in_ZFC]
empty_function_well_definedness [lemma, in FunctionsInZFC.Functions_in_ZFC]
empty_function_relation [lemma, in FunctionsInZFC.Functions_in_ZFC]
Ens [axiom, in FunctionsInZFC.Functions_in_ZFC]
EQ [record, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.stepback [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.stepfor [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.h [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.B [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.A [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric [section, in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive.A [variable, in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive [section, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans [lemma, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.C [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof [section, in FunctionsInZFC.Functions_in_ZFC]
EQ_symm [lemma, in FunctionsInZFC.Functions_in_ZFC]
EQ_refl [lemma, in FunctionsInZFC.Functions_in_ZFC]
EQ_backwards [projection, in FunctionsInZFC.Functions_in_ZFC]
EQ_forwards [projection, in FunctionsInZFC.Functions_in_ZFC]
EV [definition, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof [section, in FunctionsInZFC.Functions_in_ZFC]
EV_in_range [lemma, in FunctionsInZFC.Functions_in_ZFC]
EV_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
EV_pr [lemma, in FunctionsInZFC.Functions_in_ZFC]
excluded_middle [axiom, in FunctionsInZFC.Functions_in_ZFC]
EXISTS [definition, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.p [variable, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Extensionality [axiom, in FunctionsInZFC.Functions_in_ZFC]
Extensionality_for_functions [lemma, in FunctionsInZFC.Functions_in_ZFC]
Extensionally_equivalent [definition, in FunctionsInZFC.Functions_in_ZFC]
ex_eq_sub [lemma, in FunctionsInZFC.Functions_in_ZFC]
ex_eq_symm [lemma, in FunctionsInZFC.Functions_in_ZFC]
F
false_implies_everything [lemma, in FunctionsInZFC.Functions_in_ZFC]fe_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
First [definition, in FunctionsInZFC.Functions_in_ZFC]
First_uniqueness [lemma, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.iBF [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.iAF [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.FsubG [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.G [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.F [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.m [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.B [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.A [variable, in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness [section, in FunctionsInZFC.Functions_in_ZFC]
Functions_in_ZFC [library]
function_evaluation [lemma, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.f [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof [section, in FunctionsInZFC.Functions_in_ZFC]
function_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
function_1_Out_F [lemma, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.V [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.f [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
function_section_1 [section, in FunctionsInZFC.Functions_in_ZFC]
function_is_a_function_on [lemma, in FunctionsInZFC.Functions_in_ZFC]
function_on_dom [projection, in FunctionsInZFC.Functions_in_ZFC]
function_on_fn [projection, in FunctionsInZFC.Functions_in_ZFC]
function_sub [lemma, in FunctionsInZFC.Functions_in_ZFC]
function_well_definedness [projection, in FunctionsInZFC.Functions_in_ZFC]
function_is_a_relation [projection, in FunctionsInZFC.Functions_in_ZFC]
G
gd1a_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]gd1b_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gd2A_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gd2B_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gd2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
given_an_element_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
given_an_element.m [variable, in FunctionsInZFC.Functions_in_ZFC]
given_an_element.k [variable, in FunctionsInZFC.Functions_in_ZFC]
given_an_element.X [variable, in FunctionsInZFC.Functions_in_ZFC]
given_an_element.A [variable, in FunctionsInZFC.Functions_in_ZFC]
given_an_element [section, in FunctionsInZFC.Functions_in_ZFC]
gluA_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gluB_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gluC_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gluD_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_th5 [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluD.i1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluD.j1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluD [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep7 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep6a [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep6 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep5 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep4 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep3 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.i1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.j1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep7 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep6 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep5 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep4 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep3 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.i1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.j1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluA.i1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluA.j1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluA [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.j [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.i [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.X [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.H [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.g [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.f [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.G [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_proof [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.x1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.x1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.H [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.x [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.G [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.F [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2 [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1b.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1b.p2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1b [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1a.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1a.p1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1a [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.x [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.G [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1 [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr2.x2 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr2 [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr1.x1 [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr1 [section, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.x [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.H [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.g [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.f [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.G [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof [section, in FunctionsInZFC.Functions_in_ZFC]
glu_wd_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gr_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gr1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
gr2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
H
has_geq_2_elements_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]has_geq_2_elements [definition, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_elements_implies_leq_1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.k [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.q [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1 [section, in FunctionsInZFC.Functions_in_ZFC]
has_leq_1_elements [definition, in FunctionsInZFC.Functions_in_ZFC]
has_geq_1_elements_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
has_geq_1_elements [definition, in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_elements [definition, in FunctionsInZFC.Functions_in_ZFC]
I
ieieep_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]ieieep1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
ieieep2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
IN [axiom, in FunctionsInZFC.Functions_in_ZFC]
Infinity_exists [axiom, in FunctionsInZFC.Functions_in_ZFC]
Intersection [definition, in FunctionsInZFC.Functions_in_ZFC]
intersection [definition, in FunctionsInZFC.Functions_in_ZFC]
IntersectionProp [definition, in FunctionsInZFC.Functions_in_ZFC]
Intersection_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Intersection_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Intersection_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Intersection_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Intersection_Bounded [definition, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1_1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.Intersection_section1_1.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.Intersection_section1_1.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.Intersection_section1_1 [section, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1 [section, in FunctionsInZFC.Functions_in_ZFC]
intersection_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
intersection_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
intersection_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
intersection_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
intersection4 [section, in FunctionsInZFC.Functions_in_ZFC]
intersection4_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
intersection4.A [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.B [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.C [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.i [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.s [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.t [variable, in FunctionsInZFC.Functions_in_ZFC]
intersection4.X [variable, in FunctionsInZFC.Functions_in_ZFC]
inverse_EV_in_domain [lemma, in FunctionsInZFC.Functions_in_ZFC]
inverse_EV_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
inverse_EV_pr [lemma, in FunctionsInZFC.Functions_in_ZFC]
inverse_EV [definition, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.step0 [variable, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof [section, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded [lemma, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.U [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1 [section, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof [section, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_pr2 [projection, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_pr1 [projection, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_pair [projection, in FunctionsInZFC.Functions_in_ZFC]
in_cartesian [record, in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero [lemma, in FunctionsInZFC.Functions_in_ZFC]
in_iff_strictsub_Zero_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof [section, in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub [definition, in FunctionsInZFC.Functions_in_ZFC]
is_a_function_on [record, in FunctionsInZFC.Functions_in_ZFC]
is_a_function [record, in FunctionsInZFC.Functions_in_ZFC]
is_a_relation [definition, in FunctionsInZFC.Functions_in_ZFC]
is_a_pair [definition, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.h2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty [definition, in FunctionsInZFC.Functions_in_ZFC]
Its_empty_emptyset [lemma, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset [lemma, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2.step2_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2.i [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2 [section, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1 [section, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Its_empty [definition, in FunctionsInZFC.Functions_in_ZFC]
N
Naturals [definition, in FunctionsInZFC.Functions_in_ZFC]naturals_main_th3_rewrite [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th2_rewrite [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_next_1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_next [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.sublemma3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.sublemma2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3em_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.step3_3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.step3_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3b_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b4 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3bI_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.step3bI3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.step3bI2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.step3bI1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.s [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.subAX [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.subXA [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.r_bis [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.r [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.step3_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3a_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a.step3a2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a.step3a1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a.q [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.contra [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.p [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.X [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3 [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.sublemma1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_4 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2c_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c4 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.n [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2b_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2b.step2b1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2b.m [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2b [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2a_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.step2a3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.step2a2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.step2a1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.l [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.k [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2 [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.sub_A_N [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.in_A_N [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.N [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.h2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.h1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.h [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.A [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_ind_for_Zero [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_ind2 [projection, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_ind1 [projection, in FunctionsInZFC.Functions_in_ZFC]
naturals_main_ind_hyp [record, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA [lemma, in FunctionsInZFC.Functions_in_ZFC]
naturals_induction_nexts [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.p [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.step1_2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.N [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.h [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1 [section, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.S [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.IH_nexts [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.IH_zero [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Naturals_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Naturals_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
NEQ [definition, in FunctionsInZFC.Functions_in_ZFC]
NEQ_symm [lemma, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof [section, in FunctionsInZFC.Functions_in_ZFC]
nested_IN_bc [projection, in FunctionsInZFC.Functions_in_ZFC]
nested_IN_ab [projection, in FunctionsInZFC.Functions_in_ZFC]
nested_IN [record, in FunctionsInZFC.Functions_in_ZFC]
Next [definition, in FunctionsInZFC.Functions_in_ZFC]
Nexts_in_Naturals [lemma, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN [lemma, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.j [variable, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.N [variable, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Nothing_strictsub_Zero [lemma, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.h [variable, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.X [variable, in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero [section, in FunctionsInZFC.Functions_in_ZFC]
not_in_itself_Zero_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
not_in_itself_Zero.h [variable, in FunctionsInZFC.Functions_in_ZFC]
not_in_itself_Zero [section, in FunctionsInZFC.Functions_in_ZFC]
not_in_itself [definition, in FunctionsInZFC.Functions_in_ZFC]
O
one_different_from_two_Out [definition, in FunctionsInZFC.Functions_in_ZFC]one_different_from_two.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.h [variable, in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.n [variable, in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.m [variable, in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.X [variable, in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two [section, in FunctionsInZFC.Functions_in_ZFC]
P
PAIR [definition, in FunctionsInZFC.Functions_in_ZFC]pairwise_EQ_bd [projection, in FunctionsInZFC.Functions_in_ZFC]
pairwise_EQ_ac [projection, in FunctionsInZFC.Functions_in_ZFC]
pairwise_EQ [record, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N12 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M12 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N2 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N1 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M2 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M1 [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.f [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.n [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M [variable, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof [section, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.M [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof [section, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj1_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_uni_bd [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_uni_ac [lemma, in FunctionsInZFC.Functions_in_ZFC]
PAIR_uniqueness [lemma, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.secD [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.secB [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.fC [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.fA [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.e [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.D [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.C [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof [section, in FunctionsInZFC.Functions_in_ZFC]
PowerPlus [definition, in FunctionsInZFC.Functions_in_ZFC]
PowerPlus_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
PowerPlus_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
powerplus1 [section, in FunctionsInZFC.Functions_in_ZFC]
powerplus1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.P [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.PP [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step8 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step9 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.x [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.y [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2 [section, in FunctionsInZFC.Functions_in_ZFC]
powerplus2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.A [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.B [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.U [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.x [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.y [variable, in FunctionsInZFC.Functions_in_ZFC]
powerplus2.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
Powerset [definition, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th7 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th6 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th5 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Powerset_bounded [axiom, in FunctionsInZFC.Functions_in_ZFC]
PowerTotal [definition, in FunctionsInZFC.Functions_in_ZFC]
PowerTotal_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
PowerTotal_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
power0 [section, in FunctionsInZFC.Functions_in_ZFC]
power0_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
power0.A [variable, in FunctionsInZFC.Functions_in_ZFC]
power0.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
power1 [section, in FunctionsInZFC.Functions_in_ZFC]
power1_Out2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
power1_Out1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
power1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.x [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.y [variable, in FunctionsInZFC.Functions_in_ZFC]
power1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
power2 [section, in FunctionsInZFC.Functions_in_ZFC]
power2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
power2.A [variable, in FunctionsInZFC.Functions_in_ZFC]
power2.i [variable, in FunctionsInZFC.Functions_in_ZFC]
power2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
power2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
power3 [section, in FunctionsInZFC.Functions_in_ZFC]
power3_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
power3.A [variable, in FunctionsInZFC.Functions_in_ZFC]
power3.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
power3.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
power3.x [variable, in FunctionsInZFC.Functions_in_ZFC]
power3.X [variable, in FunctionsInZFC.Functions_in_ZFC]
power3.y [variable, in FunctionsInZFC.Functions_in_ZFC]
power3.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
power4 [section, in FunctionsInZFC.Functions_in_ZFC]
power4_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
power4.A [variable, in FunctionsInZFC.Functions_in_ZFC]
power4.P [variable, in FunctionsInZFC.Functions_in_ZFC]
power4.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
power4.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
power4.sX [variable, in FunctionsInZFC.Functions_in_ZFC]
power4.x [variable, in FunctionsInZFC.Functions_in_ZFC]
power4.X [variable, in FunctionsInZFC.Functions_in_ZFC]
power5 [section, in FunctionsInZFC.Functions_in_ZFC]
power5_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
power5.a [variable, in FunctionsInZFC.Functions_in_ZFC]
power5.A [variable, in FunctionsInZFC.Functions_in_ZFC]
power5.B [variable, in FunctionsInZFC.Functions_in_ZFC]
power5.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
power5.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
power5.x [variable, in FunctionsInZFC.Functions_in_ZFC]
power5.X [variable, in FunctionsInZFC.Functions_in_ZFC]
PR1 [definition, in FunctionsInZFC.Functions_in_ZFC]
PR2 [definition, in FunctionsInZFC.Functions_in_ZFC]
R
Range [definition, in FunctionsInZFC.Functions_in_ZFC]Range_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Range_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.p [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1 [section, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.T [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Range_prop [definition, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian [lemma, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.r [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof [section, in FunctionsInZFC.Functions_in_ZFC]
relation_sub [lemma, in FunctionsInZFC.Functions_in_ZFC]
relation_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
relation_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1.h [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1.S [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1.r [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1.R [variable, in FunctionsInZFC.Functions_in_ZFC]
relation_1 [section, in FunctionsInZFC.Functions_in_ZFC]
Relation_Total_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Relation_Total_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
remaining_property [projection, in FunctionsInZFC.Functions_in_ZFC]
REPLACEMENT [axiom, in FunctionsInZFC.Functions_in_ZFC]
REPLACEMENT_pr2 [axiom, in FunctionsInZFC.Functions_in_ZFC]
REPLACEMENT_pr1 [axiom, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th9 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th8 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th7 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th6 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th5 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb7 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb6 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb5 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb4 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb3 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.U [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb2 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb1 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.i [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.X [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b [section, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa6 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa5 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa4 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa3 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.U [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa2 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa1 [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.i [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.X [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a [section, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1 [section, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
restricted_to [definition, in FunctionsInZFC.Functions_in_ZFC]
Restriction [record, in FunctionsInZFC.Functions_in_ZFC]
Restriction_bounded [lemma, in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.t [variable, in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.R [variable, in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof [section, in FunctionsInZFC.Functions_in_ZFC]
res_to_3_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.i [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.X [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.f [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.F [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3.A [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_3 [section, in FunctionsInZFC.Functions_in_ZFC]
res_to_2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.M [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.X [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.i [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.U [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.s [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.f [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.F [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2.A [variable, in FunctionsInZFC.Functions_in_ZFC]
res_to_2 [section, in FunctionsInZFC.Functions_in_ZFC]
res_to_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
res_to_1b_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
res_to_1a_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
S
Second [definition, in FunctionsInZFC.Functions_in_ZFC]Second_uniqueness [lemma, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.sB [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.sA [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Second_has_geq_2_elements [lemma, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
second_geq_2_a_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.second_geq_2_a.stepa_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.second_geq_2_a.m [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.second_geq_2_a [section, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.E [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.sA [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Set_containing_NN_pr [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_containing_NN [definition, in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_Of_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_Of_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Set_Of [definition, in FunctionsInZFC.Functions_in_ZFC]
Singleton [axiom, in FunctionsInZFC.Functions_in_ZFC]
Singletons_have_leq_1_elements [lemma, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.iYS [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.iXS [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.S [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Singletons_have_geq_1_elements [lemma, in FunctionsInZFC.Functions_in_ZFC]
Singleton_uniqueness [lemma, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_sub1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.h2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.C [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1 [section, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Singleton_pr2 [axiom, in FunctionsInZFC.Functions_in_ZFC]
Singleton_pr1 [axiom, in FunctionsInZFC.Functions_in_ZFC]
some_things_strictsub_their_nexts [lemma, in FunctionsInZFC.Functions_in_ZFC]
stepA6 [lemma, in FunctionsInZFC.Functions_in_ZFC]
stepB6 [lemma, in FunctionsInZFC.Functions_in_ZFC]
step2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
step5 [lemma, in FunctionsInZFC.Functions_in_ZFC]
step8 [lemma, in FunctionsInZFC.Functions_in_ZFC]
StrictSUB [record, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.k [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1 [section, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.N [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof [section, in FunctionsInZFC.Functions_in_ZFC]
StrictSUB_trans1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1a_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.m [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a [section, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.h2 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.h1 [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.C [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
StrictSUB_neq [projection, in FunctionsInZFC.Functions_in_ZFC]
StrictSUB_sub [projection, in FunctionsInZFC.Functions_in_ZFC]
SUB [definition, in FunctionsInZFC.Functions_in_ZFC]
SUBPROP [definition, in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive.h [variable, in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive.B [variable, in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive.A [variable, in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive [section, in FunctionsInZFC.Functions_in_ZFC]
Substitute [lemma, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans [lemma, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.C [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof [section, in FunctionsInZFC.Functions_in_ZFC]
SUB_refl [lemma, in FunctionsInZFC.Functions_in_ZFC]
T
the_restriction [projection, in FunctionsInZFC.Functions_in_ZFC]Total [definition, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1_OutB [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1_OutA [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.B [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.A [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.R [variable, in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1 [section, in FunctionsInZFC.Functions_in_ZFC]
Total_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th4_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.l [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.j [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.W [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Total_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th3_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.j [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Total_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th2_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.j [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Total_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
U
Union [definition, in FunctionsInZFC.Functions_in_ZFC]union [axiom, in FunctionsInZFC.Functions_in_ZFC]
UnionPlus [definition, in FunctionsInZFC.Functions_in_ZFC]
UnionPlus_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
UnionPlus_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Union_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th1_OutA [lemma, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.F [variable, in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate_pr [lemma, in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate [definition, in FunctionsInZFC.Functions_in_ZFC]
Union_pr2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
Union_pr1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_symm [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.V [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_refl [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_th4 [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th4_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4b.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4b.k [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4b [section, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4a.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4a.j [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4a [section, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.contra [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra [section, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.b [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.a [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.i [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.P [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_th3 [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step7 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step6 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step5 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.X_in_V [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.U_sub_V [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.B_sub_V_proof1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.B_sub_V_proof1.h3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.B_sub_V_proof1 [section, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.h2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.step4 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.step3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.A_sub_V_proof1.step1_1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.A_sub_V_proof1.h3 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.A_sub_V_proof1 [section, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.h2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.V_pr2 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.V_pr1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.V [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.b [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_property_not_equal_X [projection, in FunctionsInZFC.Functions_in_ZFC]
union_th3_property_in_the_union [projection, in FunctionsInZFC.Functions_in_ZFC]
union_th3_property [record, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.m [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_th2 [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th2_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof [section, in FunctionsInZFC.Functions_in_ZFC]
union_th1 [lemma, in FunctionsInZFC.Functions_in_ZFC]
union_th1_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.h [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.U [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.B [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.A [variable, in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof [section, in FunctionsInZFC.Functions_in_ZFC]
Union_bounded [axiom, in FunctionsInZFC.Functions_in_ZFC]
union_pr3 [axiom, in FunctionsInZFC.Functions_in_ZFC]
union_pr2 [axiom, in FunctionsInZFC.Functions_in_ZFC]
union_pr1 [axiom, in FunctionsInZFC.Functions_in_ZFC]
W
well_definedness_sub [lemma, in FunctionsInZFC.Functions_in_ZFC]well_def_1_Out [lemma, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.step2 [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.j [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.i [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.Z [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.X [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.h [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.R [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.w [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1.F [variable, in FunctionsInZFC.Functions_in_ZFC]
well_def_1 [section, in FunctionsInZFC.Functions_in_ZFC]
well_definedness [definition, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.h [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.m [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.l [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.k [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.X [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.A [variable, in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements [section, in FunctionsInZFC.Functions_in_ZFC]
Z
Zero [definition, in FunctionsInZFC.Functions_in_ZFC]zero_not_in_itself [lemma, in FunctionsInZFC.Functions_in_ZFC]
Zero_in_Naturals [lemma, in FunctionsInZFC.Functions_in_ZFC]
Zero_element_of_NN [lemma, in FunctionsInZFC.Functions_in_ZFC]
Zero_element_of_NN_proof_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
Zero_element_of_NN_proof.k [variable, in FunctionsInZFC.Functions_in_ZFC]
Zero_element_of_NN_proof.X [variable, in FunctionsInZFC.Functions_in_ZFC]
Zero_element_of_NN_proof [section, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one_Out [definition, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.step1 [variable, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.h [variable, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.n [variable, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.m [variable, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.Y [variable, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.X [variable, in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one [section, in FunctionsInZFC.Functions_in_ZFC]
zero_has_leq_0_elements [lemma, in FunctionsInZFC.Functions_in_ZFC]
Variable Index
A
A_in_next_A_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]A_in_next_A_proof.N [in FunctionsInZFC.Functions_in_ZFC]
A_in_next_A_proof.A [in FunctionsInZFC.Functions_in_ZFC]
A_sub_next_A_proof.N [in FunctionsInZFC.Functions_in_ZFC]
A_sub_next_A_proof.A [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.M [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.B [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof.A [in FunctionsInZFC.Functions_in_ZFC]
B
big_extensionality_proof.iYS [in FunctionsInZFC.Functions_in_ZFC]big_extensionality_proof.iXS [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.S [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.eYX [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.iYD [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.iXD [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.D [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.k [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.m [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.X [in FunctionsInZFC.Functions_in_ZFC]
big_extensionality_proof.P [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.Bounded_NN_proof2.w [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.Bounded_NN_proof2.Z [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.v [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.B [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof.u [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.step1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.h [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.A [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.b [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.s [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.Q [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2.P [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1.step1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1.k [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1.X [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.h [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.A [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.s [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.Q [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.P [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.A [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof.P [in FunctionsInZFC.Functions_in_ZFC]
C
cartesian_is_relation_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]cartesian_is_relation_proof.i [in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.U [in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.B [in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_proof.A [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step9 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step8 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step7 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step6 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step5 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step4 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step3 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step2 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.Y1 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.X1 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.step1 [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.U [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.j [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.i [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.Y [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.X [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.B [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_section.A [in FunctionsInZFC.Functions_in_ZFC]
cartpair.A [in FunctionsInZFC.Functions_in_ZFC]
cartpair.B [in FunctionsInZFC.Functions_in_ZFC]
cartpair.i [in FunctionsInZFC.Functions_in_ZFC]
cartpair.step1 [in FunctionsInZFC.Functions_in_ZFC]
cartpair.step2 [in FunctionsInZFC.Functions_in_ZFC]
cartpair.step3 [in FunctionsInZFC.Functions_in_ZFC]
cartpair.step4 [in FunctionsInZFC.Functions_in_ZFC]
cartpair.U [in FunctionsInZFC.Functions_in_ZFC]
cartpair.X [in FunctionsInZFC.Functions_in_ZFC]
cartpair.X1 [in FunctionsInZFC.Functions_in_ZFC]
cartpair.Y [in FunctionsInZFC.Functions_in_ZFC]
cartpair.Y1 [in FunctionsInZFC.Functions_in_ZFC]
COMPp.F [in FunctionsInZFC.Functions_in_ZFC]
COMPp.G [in FunctionsInZFC.Functions_in_ZFC]
COMPp.i [in FunctionsInZFC.Functions_in_ZFC]
COMPp.step1 [in FunctionsInZFC.Functions_in_ZFC]
COMPp.step2 [in FunctionsInZFC.Functions_in_ZFC]
COMPp.step3 [in FunctionsInZFC.Functions_in_ZFC]
COMPp.step4 [in FunctionsInZFC.Functions_in_ZFC]
COMPp.step5 [in FunctionsInZFC.Functions_in_ZFC]
COMPp.X [in FunctionsInZFC.Functions_in_ZFC]
COMPp.Y [in FunctionsInZFC.Functions_in_ZFC]
COMPp.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step10 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step9 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step8 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step7 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step6 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step5 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step4 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step3 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.Y [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.W [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.X [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.p [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.P [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.H [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.G [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2.F [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step10 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step9 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step8 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step7 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step6 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step5 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step4 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step3 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.Y [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.W [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.X [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.p [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.P [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.H [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.G [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1.F [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step5 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step4 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step3 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.W [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.j [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.i [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.g [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.f [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.X [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.G [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3.F [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.Y [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.j [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.i [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.X [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.G [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2.F [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step9 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step8 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step7 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step6 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step5 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step4 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step3 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.W [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.j [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.i [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.Y [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.X [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.G [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1.F [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step6 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step5 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step4 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step3 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.W [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.V [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.j [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.i [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.Z [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.Y [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.X [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.g [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.f [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.G [in FunctionsInZFC.Functions_in_ZFC]
comp_wd.F [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step4 [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step3 [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step2 [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.step1 [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.c [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.X [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.G [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3.F [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step13 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step12 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB5 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB4 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB3 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB2 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.stepB1 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B.iB [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step11 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA5 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA4 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA3 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA2 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.stepA1 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A.iA [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step10 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step9 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.GB [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.GA [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.FB [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.FA [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step8 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step7 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step6 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step5 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step4 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step3 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step2 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.step1 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.contra [in FunctionsInZFC.Functions_in_ZFC]
covering_1.iX [in FunctionsInZFC.Functions_in_ZFC]
covering_1.step0a [in FunctionsInZFC.Functions_in_ZFC]
covering_1.U [in FunctionsInZFC.Functions_in_ZFC]
covering_1.jx [in FunctionsInZFC.Functions_in_ZFC]
covering_1.ix [in FunctionsInZFC.Functions_in_ZFC]
covering_1.X [in FunctionsInZFC.Functions_in_ZFC]
covering_1.j [in FunctionsInZFC.Functions_in_ZFC]
covering_1.i [in FunctionsInZFC.Functions_in_ZFC]
covering_1.v [in FunctionsInZFC.Functions_in_ZFC]
covering_1.u [in FunctionsInZFC.Functions_in_ZFC]
covering_1.g [in FunctionsInZFC.Functions_in_ZFC]
covering_1.f [in FunctionsInZFC.Functions_in_ZFC]
covering_1.G [in FunctionsInZFC.Functions_in_ZFC]
covering_1.F [in FunctionsInZFC.Functions_in_ZFC]
covering_1.B [in FunctionsInZFC.Functions_in_ZFC]
covering_1.A [in FunctionsInZFC.Functions_in_ZFC]
D
distinct_doubletons_have_geq_2_elements_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]distinct_doubletons_have_geq_2_elements_proof.iYD [in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.iXD [in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.h [in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.D [in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.n [in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
distinct_doubletons_have_geq_2_elements_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.i [in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_proof.R [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.Y [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.p [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1.X [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.T [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.R [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.conclusionBD [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.conclusionAC [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2.step1_2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2.k [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_1.step1_2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_1.k [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iBdoub [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iAdoub [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iB [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.iA [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.Doub [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.e [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.nD [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.pC [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.nB [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.pA [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.D [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.C [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.B [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.A [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.P [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.n [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.k [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof.X [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.m [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.k [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof.X [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2.step2_2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2.step2_1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2.u [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1.step1_2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1.u [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.sY [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.sX [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.D [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.n [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.m [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.k [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.X [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.sYsubA [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.sXsubA [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.D [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.iYA [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.iXA [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.A [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof.X [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.iYsY [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.D [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof.X [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.iXsX [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.D [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
E
ee_eq_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]ee_eq_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.e [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.d [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.g [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.f [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.G [in FunctionsInZFC.Functions_in_ZFC]
ee_eq_proof.F [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step12 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step11 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step10a [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step10 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step9 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.W [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step8 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step7 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.V [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.X [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.i [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.M [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.e [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.s [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.g [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.f [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.G [in FunctionsInZFC.Functions_in_ZFC]
ee_sub_proof.F [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.j [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.i [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.X [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.e [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.G [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof.F [in FunctionsInZFC.Functions_in_ZFC]
efdom.i [in FunctionsInZFC.Functions_in_ZFC]
efdom.step1 [in FunctionsInZFC.Functions_in_ZFC]
efdom.X [in FunctionsInZFC.Functions_in_ZFC]
efdom.Y [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.step1 [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.i [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.Z [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.Y [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2.X [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1.i [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1.X [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.step2 [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2.step1 [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2.h [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2.B [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.A [in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty.h [in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty.X [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.stepback [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.stepfor [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.h [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.B [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric.A [in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive.A [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.k [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.h [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.C [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.B [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof.A [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.i [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.X [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof.R [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.p [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof.P [in FunctionsInZFC.Functions_in_ZFC]
F
first_uniqueness.step1 [in FunctionsInZFC.Functions_in_ZFC]first_uniqueness.iBF [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.iAF [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.FsubG [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.G [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.F [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.m [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.B [in FunctionsInZFC.Functions_in_ZFC]
first_uniqueness.A [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.i [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.f [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.X [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation_proof.F [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.step5 [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.step3 [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.V [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.i [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.Y [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.X [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.f [in FunctionsInZFC.Functions_in_ZFC]
function_section_1.F [in FunctionsInZFC.Functions_in_ZFC]
G
given_an_element.m [in FunctionsInZFC.Functions_in_ZFC]given_an_element.k [in FunctionsInZFC.Functions_in_ZFC]
given_an_element.X [in FunctionsInZFC.Functions_in_ZFC]
given_an_element.A [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step8 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.step7 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.step6 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluD.i1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluD.j1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep7 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep6a [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep6 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep5 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep4 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep3 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.Cstep1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.i1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC.j1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep7 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep6 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep5 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep4 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep3 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.Bstep1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.i1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB.j1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluA.i1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluA.j1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.j [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.i [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.Z [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.Y [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.X [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.H [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.e [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.g [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.f [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.G [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.F [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.step2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.step1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.Y [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B.x1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.step2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.step1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.Y [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A.x1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.H [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.x [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.X [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.G [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.F [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1b.step3 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1b.p2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1a.step2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1a.p1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.step1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.Y [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.x [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.X [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.G [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.F [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr2.x2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr1.x1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.x [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.X [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.H [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.g [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.f [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.G [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.F [in FunctionsInZFC.Functions_in_ZFC]
H
has_leq_0_implies_leq_1.step2 [in FunctionsInZFC.Functions_in_ZFC]has_leq_0_implies_leq_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.k [in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.Y [in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.X [in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.q [in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_implies_leq_1.A [in FunctionsInZFC.Functions_in_ZFC]
I
Intersection_section1.step2 [in FunctionsInZFC.Functions_in_ZFC]Intersection_section1.step1 [in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.Intersection_section1_1.h [in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.Intersection_section1_1.Z [in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.A [in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1.F [in FunctionsInZFC.Functions_in_ZFC]
intersection4.A [in FunctionsInZFC.Functions_in_ZFC]
intersection4.B [in FunctionsInZFC.Functions_in_ZFC]
intersection4.C [in FunctionsInZFC.Functions_in_ZFC]
intersection4.i [in FunctionsInZFC.Functions_in_ZFC]
intersection4.s [in FunctionsInZFC.Functions_in_ZFC]
intersection4.step1 [in FunctionsInZFC.Functions_in_ZFC]
intersection4.step2 [in FunctionsInZFC.Functions_in_ZFC]
intersection4.t [in FunctionsInZFC.Functions_in_ZFC]
intersection4.X [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.step0 [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.X [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.i [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof.R [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.step8 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step7 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step6 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step5 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step4 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.Y [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.X [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.step1 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.i [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1.U [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.B [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.A [in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof.h [in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.h2 [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.A [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof.X [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2.step2_1 [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2.i [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2.X [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1.i [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1.X [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.k [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.A [in FunctionsInZFC.Functions_in_ZFC]
N
naturals_main_induction_step.sublemma3 [in FunctionsInZFC.Functions_in_ZFC]naturals_main_induction_step.naturals_main_induction3.sublemma2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.step3_3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.step3_2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b4 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.step3bI3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.step3bI2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.step3bI1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI.s [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.step3b1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.subAX [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.subXA [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.r_bis [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.r [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.step3_1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a.step3a2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a.step3a1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a.q [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.contra [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.p [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.X [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.sublemma1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_4 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c4 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.step2c1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c.n [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2b.step2b1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2b.m [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.step2_1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.step2a3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.step2a2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.step2a1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a.l [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.k [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.sub_A_N [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.in_A_N [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.N [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.h2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.h1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.h [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.A [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step9 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step8 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.p [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.B [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step7 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.step1_2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.N [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.h [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1.A [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.S [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.IH_nexts [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.IH_zero [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.P [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.k [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.B [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.m [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.k [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.B [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof.A [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.j [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.N [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.k [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof.A [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.step3 [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.step2 [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.step1 [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.h [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero.X [in FunctionsInZFC.Functions_in_ZFC]
not_in_itself_Zero.h [in FunctionsInZFC.Functions_in_ZFC]
O
one_different_from_two.step1 [in FunctionsInZFC.Functions_in_ZFC]one_different_from_two.h [in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.n [in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.m [in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.Y [in FunctionsInZFC.Functions_in_ZFC]
one_different_from_two.X [in FunctionsInZFC.Functions_in_ZFC]
P
PAIR_proj_uni_proof.step9 [in FunctionsInZFC.Functions_in_ZFC]PAIR_proj_uni_proof.step8 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step7 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.U [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N12 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M12 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N2 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N1 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M2 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M1 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.f [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.e [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.n [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.N [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.m [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_uni_proof.M [in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.M [in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_proof.X [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step9 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step8 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step7 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.secD [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.secB [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.fC [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.fA [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.e [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.D [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.C [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.B [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof.A [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.A [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.P [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.PP [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step1 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step2 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step3 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step4 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step5 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step6 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step7 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step8 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.step9 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.x [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.X [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.y [in FunctionsInZFC.Functions_in_ZFC]
powerplus1.Y [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.A [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.B [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step1 [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step2 [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step3 [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.step4 [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.U [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.x [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.X [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.y [in FunctionsInZFC.Functions_in_ZFC]
powerplus2.Y [in FunctionsInZFC.Functions_in_ZFC]
power0.A [in FunctionsInZFC.Functions_in_ZFC]
power0.step1 [in FunctionsInZFC.Functions_in_ZFC]
power1.A [in FunctionsInZFC.Functions_in_ZFC]
power1.step1 [in FunctionsInZFC.Functions_in_ZFC]
power1.step2 [in FunctionsInZFC.Functions_in_ZFC]
power1.step3 [in FunctionsInZFC.Functions_in_ZFC]
power1.step4 [in FunctionsInZFC.Functions_in_ZFC]
power1.step5 [in FunctionsInZFC.Functions_in_ZFC]
power1.x [in FunctionsInZFC.Functions_in_ZFC]
power1.X [in FunctionsInZFC.Functions_in_ZFC]
power1.y [in FunctionsInZFC.Functions_in_ZFC]
power1.Y [in FunctionsInZFC.Functions_in_ZFC]
power2.A [in FunctionsInZFC.Functions_in_ZFC]
power2.i [in FunctionsInZFC.Functions_in_ZFC]
power2.step1 [in FunctionsInZFC.Functions_in_ZFC]
power2.X [in FunctionsInZFC.Functions_in_ZFC]
power3.A [in FunctionsInZFC.Functions_in_ZFC]
power3.step1 [in FunctionsInZFC.Functions_in_ZFC]
power3.step2 [in FunctionsInZFC.Functions_in_ZFC]
power3.x [in FunctionsInZFC.Functions_in_ZFC]
power3.X [in FunctionsInZFC.Functions_in_ZFC]
power3.y [in FunctionsInZFC.Functions_in_ZFC]
power3.Y [in FunctionsInZFC.Functions_in_ZFC]
power4.A [in FunctionsInZFC.Functions_in_ZFC]
power4.P [in FunctionsInZFC.Functions_in_ZFC]
power4.step1 [in FunctionsInZFC.Functions_in_ZFC]
power4.step2 [in FunctionsInZFC.Functions_in_ZFC]
power4.sX [in FunctionsInZFC.Functions_in_ZFC]
power4.x [in FunctionsInZFC.Functions_in_ZFC]
power4.X [in FunctionsInZFC.Functions_in_ZFC]
power5.a [in FunctionsInZFC.Functions_in_ZFC]
power5.A [in FunctionsInZFC.Functions_in_ZFC]
power5.B [in FunctionsInZFC.Functions_in_ZFC]
power5.step1 [in FunctionsInZFC.Functions_in_ZFC]
power5.step2 [in FunctionsInZFC.Functions_in_ZFC]
power5.x [in FunctionsInZFC.Functions_in_ZFC]
power5.X [in FunctionsInZFC.Functions_in_ZFC]
R
Range_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]Range_th1_proof.i [in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Range_th1_proof.R [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.X [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.p [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.Range_prop_bounded_proof_1.Y [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.T [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof.R [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step7 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.X [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.i [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.U [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.B [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.A [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.r [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof.R [in FunctionsInZFC.Functions_in_ZFC]
relation_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
relation_1.i [in FunctionsInZFC.Functions_in_ZFC]
relation_1.X [in FunctionsInZFC.Functions_in_ZFC]
relation_1.h [in FunctionsInZFC.Functions_in_ZFC]
relation_1.S [in FunctionsInZFC.Functions_in_ZFC]
relation_1.r [in FunctionsInZFC.Functions_in_ZFC]
relation_1.R [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.step2 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb7 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb6 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb5 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb4 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb3 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.U [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.Y [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb2 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.stepb1 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.i [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b.X [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa6 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa5 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa4 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa3 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.U [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa2 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.stepa1 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.Y [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.i [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a.X [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.F [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.A [in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.t [in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.R [in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.A [in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof.P [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step7 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step6 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step5 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step4 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step3 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step2 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.step1 [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.Z [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.Y [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.i [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.X [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.f [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.F [in FunctionsInZFC.Functions_in_ZFC]
res_to_3.A [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step7 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step6 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step5 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step4 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step3 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step2 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.step1 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.M [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.Y [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.X [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.i [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.U [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.s [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.f [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.F [in FunctionsInZFC.Functions_in_ZFC]
res_to_2.A [in FunctionsInZFC.Functions_in_ZFC]
S
second_uniqueness_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]second_uniqueness_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.sB [in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.sA [in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.k [in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.B [in FunctionsInZFC.Functions_in_ZFC]
second_uniqueness_proof.A [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.second_geq_2_a.stepa_1 [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.second_geq_2_a.m [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.E [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.sA [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.k [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof.A [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.iYS [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.iXS [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.X [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.S [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof.A [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.B [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.step2 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.step1 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.h2 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1.C [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.B [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.A [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.step4 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.step3 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.step2 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1.k [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.N [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.h [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.A [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.step4 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.step3 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.step2 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a.m [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.h2 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.h1 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.k [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.C [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.B [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.A [in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive.h [in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive.B [in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive.A [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.m [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.X [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.k [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.h [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.C [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.B [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof.A [in FunctionsInZFC.Functions_in_ZFC]
T
total_and_pairs_1.step5 [in FunctionsInZFC.Functions_in_ZFC]total_and_pairs_1.step4 [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step3 [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step2 [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.i [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.B [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.A [in FunctionsInZFC.Functions_in_ZFC]
total_and_pairs_1.R [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.l [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.k [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.j [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.i [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.F [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.W [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
total_th4_proof.X [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.k [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.j [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.i [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.F [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof.X [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.j [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.i [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.F [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.Y [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof.X [in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.i [in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.F [in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
U
Union_th1_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]Union_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.k [in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.U [in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
Union_th1_proof.F [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.V [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.U [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.B [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof.A [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.U [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof.A [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.step7 [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.step6 [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4b.step4 [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4b.k [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.step3 [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4a.step1 [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4a.j [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.contra [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.b [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.a [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.i [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.X [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.B [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.A [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.P [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step7 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step6 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step5 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.X_in_V [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.U_sub_V [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.B_sub_V_proof1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.B_sub_V_proof1.h3 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.h2 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.step4 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.step3 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.step2 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.A_sub_V_proof1.step1_1 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.A_sub_V_proof1.h3 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.h2 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.Z [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.V_pr2 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.V_pr1 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.V [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.b [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.m [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.k [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.h [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.X [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.U [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.h [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.X [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.U [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.B [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof.A [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.step1 [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.h [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.X [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.U [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.B [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof.A [in FunctionsInZFC.Functions_in_ZFC]
W
well_def_1.step2 [in FunctionsInZFC.Functions_in_ZFC]well_def_1.step1 [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.j [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.i [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.Z [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.Y [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.X [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.h [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.R [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.w [in FunctionsInZFC.Functions_in_ZFC]
well_def_1.F [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.h [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.m [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.l [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.k [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.Y [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.X [in FunctionsInZFC.Functions_in_ZFC]
when_given_two_distinct_elements.A [in FunctionsInZFC.Functions_in_ZFC]
Z
Zero_element_of_NN_proof.k [in FunctionsInZFC.Functions_in_ZFC]Zero_element_of_NN_proof.X [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.step1 [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.h [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.n [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.m [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.Y [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one.X [in FunctionsInZFC.Functions_in_ZFC]
Library Index
F
Functions_in_ZFCLemma Index
A
anything_in_next_of_itself [in FunctionsInZFC.Functions_in_ZFC]anything_sub_next_of_itself [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_th2 [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair [in FunctionsInZFC.Functions_in_ZFC]
A_sub_V_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
B
Big_Extensionality [in FunctionsInZFC.Functions_in_ZFC]Bounded_NN [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_pre [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops_th2 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_sub2_Out [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops_th1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_CHOICE_pr [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th2 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1 [in FunctionsInZFC.Functions_in_ZFC]
B_sub_V_proof1_Out [in FunctionsInZFC.Functions_in_ZFC]
C
cartesian_subs_are_relations [in FunctionsInZFC.Functions_in_ZFC]cartesian_is_relation [in FunctionsInZFC.Functions_in_ZFC]
cartesian_is_relation_Out [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pair_th2 [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pair_th1 [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_proj2_th [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_proj1_th [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_th1 [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_construction [in FunctionsInZFC.Functions_in_ZFC]
cartesian_construction_Out [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Cartesian_pr1 [in FunctionsInZFC.Functions_in_ZFC]
cartpairA_Out [in FunctionsInZFC.Functions_in_ZFC]
cartpairB_Out [in FunctionsInZFC.Functions_in_ZFC]
Choose_an_element_pr [in FunctionsInZFC.Functions_in_ZFC]
composition_th4 [in FunctionsInZFC.Functions_in_ZFC]
composition_th3 [in FunctionsInZFC.Functions_in_ZFC]
composition_th2 [in FunctionsInZFC.Functions_in_ZFC]
composition_th1 [in FunctionsInZFC.Functions_in_ZFC]
composition_well_definedness [in FunctionsInZFC.Functions_in_ZFC]
composition_bounded [in FunctionsInZFC.Functions_in_ZFC]
composition_bounded_by [in FunctionsInZFC.Functions_in_ZFC]
COMPp_Out4 [in FunctionsInZFC.Functions_in_ZFC]
COMPp_Out3 [in FunctionsInZFC.Functions_in_ZFC]
COMP_assoc [in FunctionsInZFC.Functions_in_ZFC]
COMP_assoc_th2 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2_Out [in FunctionsInZFC.Functions_in_ZFC]
COMP_assoc_th1 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1_Out [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3_Out [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2_Out [in FunctionsInZFC.Functions_in_ZFC]
COMP_th5 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1_Out [in FunctionsInZFC.Functions_in_ZFC]
comp_wd_Out [in FunctionsInZFC.Functions_in_ZFC]
COMP_th4p [in FunctionsInZFC.Functions_in_ZFC]
COMP_th3p [in FunctionsInZFC.Functions_in_ZFC]
COMP_th4 [in FunctionsInZFC.Functions_in_ZFC]
COMP_th3 [in FunctionsInZFC.Functions_in_ZFC]
COMP_th2 [in FunctionsInZFC.Functions_in_ZFC]
COMP_th1 [in FunctionsInZFC.Functions_in_ZFC]
COMP_pr2 [in FunctionsInZFC.Functions_in_ZFC]
COMP_pr1 [in FunctionsInZFC.Functions_in_ZFC]
Comp_prop_th3 [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3_Out [in FunctionsInZFC.Functions_in_ZFC]
Comp_prop_th2 [in FunctionsInZFC.Functions_in_ZFC]
Comp_prop_th1 [in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER_th2 [in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER_th1 [in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER_pr1 [in FunctionsInZFC.Functions_in_ZFC]
Contains_NN_Naturals [in FunctionsInZFC.Functions_in_ZFC]
counting_lem2 [in FunctionsInZFC.Functions_in_ZFC]
counting_lem1 [in FunctionsInZFC.Functions_in_ZFC]
covering_th2 [in FunctionsInZFC.Functions_in_ZFC]
covering_th1 [in FunctionsInZFC.Functions_in_ZFC]
covering_1_Out [in FunctionsInZFC.Functions_in_ZFC]
covering_em_Out [in FunctionsInZFC.Functions_in_ZFC]
cpb1_Out [in FunctionsInZFC.Functions_in_ZFC]
D
distinct_Doubletons_have_geq_2_elements [in FunctionsInZFC.Functions_in_ZFC]Domain_th1 [in FunctionsInZFC.Functions_in_ZFC]
Domain_th1_Out [in FunctionsInZFC.Functions_in_ZFC]
Domain_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Domain_pr1 [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_Out [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof_1_Out [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_uniqueness [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th4_b [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th4_a [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th4 [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th3 [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th2 [in FunctionsInZFC.Functions_in_ZFC]
Doubleton_th1 [in FunctionsInZFC.Functions_in_ZFC]
E
ee_eq_Out [in FunctionsInZFC.Functions_in_ZFC]ee_sub_Out [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_Out [in FunctionsInZFC.Functions_in_ZFC]
efdom_Out [in FunctionsInZFC.Functions_in_ZFC]
emptyfn1_Out [in FunctionsInZFC.Functions_in_ZFC]
emptyfn2_Out [in FunctionsInZFC.Functions_in_ZFC]
EmptySet_th2 [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything_Out [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything_2_Out [in FunctionsInZFC.Functions_in_ZFC]
EmptySet_th1 [in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty_Out [in FunctionsInZFC.Functions_in_ZFC]
empty_function_domain [in FunctionsInZFC.Functions_in_ZFC]
empty_function_domain_empty [in FunctionsInZFC.Functions_in_ZFC]
empty_function_function [in FunctionsInZFC.Functions_in_ZFC]
empty_function_well_definedness [in FunctionsInZFC.Functions_in_ZFC]
empty_function_relation [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric_Out [in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive_Out [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
EQ_symm [in FunctionsInZFC.Functions_in_ZFC]
EQ_refl [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_Out [in FunctionsInZFC.Functions_in_ZFC]
EV_in_range [in FunctionsInZFC.Functions_in_ZFC]
EV_th1 [in FunctionsInZFC.Functions_in_ZFC]
EV_pr [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1 [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
Extensionality_for_functions [in FunctionsInZFC.Functions_in_ZFC]
ex_eq_sub [in FunctionsInZFC.Functions_in_ZFC]
ex_eq_symm [in FunctionsInZFC.Functions_in_ZFC]
F
false_implies_everything [in FunctionsInZFC.Functions_in_ZFC]fe_Out [in FunctionsInZFC.Functions_in_ZFC]
First_uniqueness [in FunctionsInZFC.Functions_in_ZFC]
function_evaluation [in FunctionsInZFC.Functions_in_ZFC]
function_th1 [in FunctionsInZFC.Functions_in_ZFC]
function_1_Out_F [in FunctionsInZFC.Functions_in_ZFC]
function_is_a_function_on [in FunctionsInZFC.Functions_in_ZFC]
function_sub [in FunctionsInZFC.Functions_in_ZFC]
G
gd1a_Out [in FunctionsInZFC.Functions_in_ZFC]gd1b_Out [in FunctionsInZFC.Functions_in_ZFC]
gd2A_Out [in FunctionsInZFC.Functions_in_ZFC]
gd2B_Out [in FunctionsInZFC.Functions_in_ZFC]
gd2_Out [in FunctionsInZFC.Functions_in_ZFC]
gluA_Out [in FunctionsInZFC.Functions_in_ZFC]
gluB_Out [in FunctionsInZFC.Functions_in_ZFC]
gluC_Out [in FunctionsInZFC.Functions_in_ZFC]
gluD_Out [in FunctionsInZFC.Functions_in_ZFC]
glueing_th5 [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
glueing_th4 [in FunctionsInZFC.Functions_in_ZFC]
glueing_th3 [in FunctionsInZFC.Functions_in_ZFC]
glueing_th2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1_Out [in FunctionsInZFC.Functions_in_ZFC]
glueing_th1 [in FunctionsInZFC.Functions_in_ZFC]
glu_wd_Out [in FunctionsInZFC.Functions_in_ZFC]
gr_Out [in FunctionsInZFC.Functions_in_ZFC]
gr1_Out [in FunctionsInZFC.Functions_in_ZFC]
gr2_Out [in FunctionsInZFC.Functions_in_ZFC]
H
has_geq_2_elements_th1 [in FunctionsInZFC.Functions_in_ZFC]has_leq_0_elements_implies_leq_1 [in FunctionsInZFC.Functions_in_ZFC]
has_geq_1_elements_th1 [in FunctionsInZFC.Functions_in_ZFC]
I
ieieep_Out [in FunctionsInZFC.Functions_in_ZFC]ieieep1_Out [in FunctionsInZFC.Functions_in_ZFC]
ieieep2_Out [in FunctionsInZFC.Functions_in_ZFC]
Intersection_th2 [in FunctionsInZFC.Functions_in_ZFC]
Intersection_th1 [in FunctionsInZFC.Functions_in_ZFC]
Intersection_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Intersection_pr1 [in FunctionsInZFC.Functions_in_ZFC]
intersection_th4 [in FunctionsInZFC.Functions_in_ZFC]
intersection_th3 [in FunctionsInZFC.Functions_in_ZFC]
intersection_th2 [in FunctionsInZFC.Functions_in_ZFC]
intersection_th1 [in FunctionsInZFC.Functions_in_ZFC]
intersection4_Out [in FunctionsInZFC.Functions_in_ZFC]
inverse_EV_in_domain [in FunctionsInZFC.Functions_in_ZFC]
inverse_EV_th1 [in FunctionsInZFC.Functions_in_ZFC]
inverse_EV_pr [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_Out [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_Out [in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_th1 [in FunctionsInZFC.Functions_in_ZFC]
Its_empty_emptyset [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset [in FunctionsInZFC.Functions_in_ZFC]
N
naturals_main_th3_rewrite [in FunctionsInZFC.Functions_in_ZFC]naturals_main_th3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th2_rewrite [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_th1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_next_1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_next [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_ind_for_Zero [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1 [in FunctionsInZFC.Functions_in_ZFC]
Naturals_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Naturals_pr1 [in FunctionsInZFC.Functions_in_ZFC]
NEQ_symm [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_Out [in FunctionsInZFC.Functions_in_ZFC]
Nexts_in_Naturals [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN [in FunctionsInZFC.Functions_in_ZFC]
Nothing_strictsub_Zero [in FunctionsInZFC.Functions_in_ZFC]
P
PAIR_proj_uni [in FunctionsInZFC.Functions_in_ZFC]PAIR_proj_th4 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th3 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th2 [in FunctionsInZFC.Functions_in_ZFC]
pair_proj2_Out [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj_th1 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_proj1_pr1 [in FunctionsInZFC.Functions_in_ZFC]
PAIR_uni_bd [in FunctionsInZFC.Functions_in_ZFC]
PAIR_uni_ac [in FunctionsInZFC.Functions_in_ZFC]
PAIR_uniqueness [in FunctionsInZFC.Functions_in_ZFC]
PowerPlus_th2 [in FunctionsInZFC.Functions_in_ZFC]
PowerPlus_th1 [in FunctionsInZFC.Functions_in_ZFC]
powerplus1_Out [in FunctionsInZFC.Functions_in_ZFC]
powerplus2_Out [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th7 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th6 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th5 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th4 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th3 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th2 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_th1 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Powerset_pr1 [in FunctionsInZFC.Functions_in_ZFC]
PowerTotal_th2 [in FunctionsInZFC.Functions_in_ZFC]
PowerTotal_th1 [in FunctionsInZFC.Functions_in_ZFC]
power0_Out [in FunctionsInZFC.Functions_in_ZFC]
power1_Out2 [in FunctionsInZFC.Functions_in_ZFC]
power1_Out1 [in FunctionsInZFC.Functions_in_ZFC]
power2_Out [in FunctionsInZFC.Functions_in_ZFC]
power3_Out [in FunctionsInZFC.Functions_in_ZFC]
power4_Out [in FunctionsInZFC.Functions_in_ZFC]
power5_Out [in FunctionsInZFC.Functions_in_ZFC]
R
Range_th1 [in FunctionsInZFC.Functions_in_ZFC]Range_th1_Out [in FunctionsInZFC.Functions_in_ZFC]
Range_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Range_pr1 [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_Out [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof_1_Out [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_Out [in FunctionsInZFC.Functions_in_ZFC]
relation_sub [in FunctionsInZFC.Functions_in_ZFC]
relation_1_Out [in FunctionsInZFC.Functions_in_ZFC]
Relation_Total_th2 [in FunctionsInZFC.Functions_in_ZFC]
Relation_Total_th1 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th9 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th8 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th7 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th6 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th5 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th4 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th3 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th2 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_th1 [in FunctionsInZFC.Functions_in_ZFC]
Restriction_bounded [in FunctionsInZFC.Functions_in_ZFC]
res_to_3_Out [in FunctionsInZFC.Functions_in_ZFC]
res_to_2_Out [in FunctionsInZFC.Functions_in_ZFC]
res_to_1_Out [in FunctionsInZFC.Functions_in_ZFC]
res_to_1b_Out [in FunctionsInZFC.Functions_in_ZFC]
res_to_1a_Out [in FunctionsInZFC.Functions_in_ZFC]
S
Second_uniqueness [in FunctionsInZFC.Functions_in_ZFC]Second_has_geq_2_elements [in FunctionsInZFC.Functions_in_ZFC]
Set_containing_NN_pr [in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th4 [in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th3 [in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th2 [in FunctionsInZFC.Functions_in_ZFC]
Set_Of_th1 [in FunctionsInZFC.Functions_in_ZFC]
Set_Of_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Set_Of_pr1 [in FunctionsInZFC.Functions_in_ZFC]
Singletons_have_leq_1_elements [in FunctionsInZFC.Functions_in_ZFC]
Singletons_have_geq_1_elements [in FunctionsInZFC.Functions_in_ZFC]
Singleton_uniqueness [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1 [in FunctionsInZFC.Functions_in_ZFC]
some_things_strictsub_their_nexts [in FunctionsInZFC.Functions_in_ZFC]
stepA6 [in FunctionsInZFC.Functions_in_ZFC]
stepB6 [in FunctionsInZFC.Functions_in_ZFC]
step2 [in FunctionsInZFC.Functions_in_ZFC]
step5 [in FunctionsInZFC.Functions_in_ZFC]
step8 [in FunctionsInZFC.Functions_in_ZFC]
StrictSUB_trans1 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_Out [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1a_Out [in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive_Out [in FunctionsInZFC.Functions_in_ZFC]
Substitute [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
SUB_refl [in FunctionsInZFC.Functions_in_ZFC]
T
total_and_pairs_1_OutB [in FunctionsInZFC.Functions_in_ZFC]total_and_pairs_1_OutA [in FunctionsInZFC.Functions_in_ZFC]
Total_th4 [in FunctionsInZFC.Functions_in_ZFC]
total_th4_Out [in FunctionsInZFC.Functions_in_ZFC]
Total_th3 [in FunctionsInZFC.Functions_in_ZFC]
total_th3_Out [in FunctionsInZFC.Functions_in_ZFC]
Total_th2 [in FunctionsInZFC.Functions_in_ZFC]
total_th2_Out [in FunctionsInZFC.Functions_in_ZFC]
Total_th1 [in FunctionsInZFC.Functions_in_ZFC]
total_th1_Out [in FunctionsInZFC.Functions_in_ZFC]
U
UnionPlus_th2 [in FunctionsInZFC.Functions_in_ZFC]UnionPlus_th1 [in FunctionsInZFC.Functions_in_ZFC]
Union_th1 [in FunctionsInZFC.Functions_in_ZFC]
union_th1_OutA [in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate_th2 [in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate_th1 [in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate_pr [in FunctionsInZFC.Functions_in_ZFC]
Union_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Union_pr1 [in FunctionsInZFC.Functions_in_ZFC]
union_symm [in FunctionsInZFC.Functions_in_ZFC]
union_symm_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
union_refl [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
union_th4 [in FunctionsInZFC.Functions_in_ZFC]
union_th4_Out [in FunctionsInZFC.Functions_in_ZFC]
union_th3 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
union_th2 [in FunctionsInZFC.Functions_in_ZFC]
union_th1 [in FunctionsInZFC.Functions_in_ZFC]
W
well_definedness_sub [in FunctionsInZFC.Functions_in_ZFC]well_def_1_Out [in FunctionsInZFC.Functions_in_ZFC]
Z
zero_not_in_itself [in FunctionsInZFC.Functions_in_ZFC]Zero_in_Naturals [in FunctionsInZFC.Functions_in_ZFC]
Zero_element_of_NN [in FunctionsInZFC.Functions_in_ZFC]
zero_has_leq_0_elements [in FunctionsInZFC.Functions_in_ZFC]
Axiom Index
C
CHOICE [in FunctionsInZFC.Functions_in_ZFC]CHOICE_pr [in FunctionsInZFC.Functions_in_ZFC]
E
EmptySet [in FunctionsInZFC.Functions_in_ZFC]EmptySet_pr [in FunctionsInZFC.Functions_in_ZFC]
Ens [in FunctionsInZFC.Functions_in_ZFC]
excluded_middle [in FunctionsInZFC.Functions_in_ZFC]
Extensionality [in FunctionsInZFC.Functions_in_ZFC]
I
IN [in FunctionsInZFC.Functions_in_ZFC]Infinity_exists [in FunctionsInZFC.Functions_in_ZFC]
P
Powerset_bounded [in FunctionsInZFC.Functions_in_ZFC]R
REPLACEMENT [in FunctionsInZFC.Functions_in_ZFC]REPLACEMENT_pr2 [in FunctionsInZFC.Functions_in_ZFC]
REPLACEMENT_pr1 [in FunctionsInZFC.Functions_in_ZFC]
S
Singleton [in FunctionsInZFC.Functions_in_ZFC]Singleton_pr2 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_pr1 [in FunctionsInZFC.Functions_in_ZFC]
U
union [in FunctionsInZFC.Functions_in_ZFC]Union_bounded [in FunctionsInZFC.Functions_in_ZFC]
union_pr3 [in FunctionsInZFC.Functions_in_ZFC]
union_pr2 [in FunctionsInZFC.Functions_in_ZFC]
union_pr1 [in FunctionsInZFC.Functions_in_ZFC]
Projection Index
C
Comp_intern [in FunctionsInZFC.Functions_in_ZFC]Comp_pair [in FunctionsInZFC.Functions_in_ZFC]
Comp_inter_yz [in FunctionsInZFC.Functions_in_ZFC]
Comp_inter_xy [in FunctionsInZFC.Functions_in_ZFC]
Contains_NN_nexts [in FunctionsInZFC.Functions_in_ZFC]
Contains_NN_zero [in FunctionsInZFC.Functions_in_ZFC]
E
EQ_backwards [in FunctionsInZFC.Functions_in_ZFC]EQ_forwards [in FunctionsInZFC.Functions_in_ZFC]
F
function_on_dom [in FunctionsInZFC.Functions_in_ZFC]function_on_fn [in FunctionsInZFC.Functions_in_ZFC]
function_well_definedness [in FunctionsInZFC.Functions_in_ZFC]
function_is_a_relation [in FunctionsInZFC.Functions_in_ZFC]
I
in_cartesian_pr2 [in FunctionsInZFC.Functions_in_ZFC]in_cartesian_pr1 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_pair [in FunctionsInZFC.Functions_in_ZFC]
N
naturals_main_ind2 [in FunctionsInZFC.Functions_in_ZFC]naturals_main_ind1 [in FunctionsInZFC.Functions_in_ZFC]
nested_IN_bc [in FunctionsInZFC.Functions_in_ZFC]
nested_IN_ab [in FunctionsInZFC.Functions_in_ZFC]
P
pairwise_EQ_bd [in FunctionsInZFC.Functions_in_ZFC]pairwise_EQ_ac [in FunctionsInZFC.Functions_in_ZFC]
R
remaining_property [in FunctionsInZFC.Functions_in_ZFC]S
StrictSUB_neq [in FunctionsInZFC.Functions_in_ZFC]StrictSUB_sub [in FunctionsInZFC.Functions_in_ZFC]
T
the_restriction [in FunctionsInZFC.Functions_in_ZFC]U
union_th3_property_not_equal_X [in FunctionsInZFC.Functions_in_ZFC]union_th3_property_in_the_union [in FunctionsInZFC.Functions_in_ZFC]
Section Index
A
A_in_next_A_proof [in FunctionsInZFC.Functions_in_ZFC]A_sub_next_A_proof [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_proof [in FunctionsInZFC.Functions_in_ZFC]
B
big_extensionality_proof [in FunctionsInZFC.Functions_in_ZFC]Bounded_NN_proof.Bounded_NN_proof2 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops2 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1.boundedsubprops1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1 [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
C
cartesian_is_relation_proof [in FunctionsInZFC.Functions_in_ZFC]cartesian_construction_section [in FunctionsInZFC.Functions_in_ZFC]
cartpair [in FunctionsInZFC.Functions_in_ZFC]
COMPp [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_2 [in FunctionsInZFC.Functions_in_ZFC]
comp_assoc_1 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_3 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_2 [in FunctionsInZFC.Functions_in_ZFC]
comp_ev_1 [in FunctionsInZFC.Functions_in_ZFC]
comp_wd [in FunctionsInZFC.Functions_in_ZFC]
comp_prop_3 [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_B [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em.covering_1_A [in FunctionsInZFC.Functions_in_ZFC]
covering_1.covering_em [in FunctionsInZFC.Functions_in_ZFC]
covering_1 [in FunctionsInZFC.Functions_in_ZFC]
D
distinct_doubletons_have_geq_2_elements_proof [in FunctionsInZFC.Functions_in_ZFC]Domain_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof.Domain_prop_bounded_proof_1 [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop_bounded_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof.doubleton_uniqueness_1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub2 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof.doubleton_th4_sub1 [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_proof [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
E
ee_eq_proof [in FunctionsInZFC.Functions_in_ZFC]ee_sub_proof [in FunctionsInZFC.Functions_in_ZFC]
ee_symm_proof [in FunctionsInZFC.Functions_in_ZFC]
efdom [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_2 [in FunctionsInZFC.Functions_in_ZFC]
emptyfn_1 [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything.emptyset_subset_everything_2 [in FunctionsInZFC.Functions_in_ZFC]
emptyset_subset_everything [in FunctionsInZFC.Functions_in_ZFC]
emptyset_empty [in FunctionsInZFC.Functions_in_ZFC]
equality_symmetric [in FunctionsInZFC.Functions_in_ZFC]
equality_reflexive [in FunctionsInZFC.Functions_in_ZFC]
EQ_trans_proof [in FunctionsInZFC.Functions_in_ZFC]
eval_in_range_proof [in FunctionsInZFC.Functions_in_ZFC]
EXISTS_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
F
first_uniqueness [in FunctionsInZFC.Functions_in_ZFC]function_evaluation_proof [in FunctionsInZFC.Functions_in_ZFC]
function_section_1 [in FunctionsInZFC.Functions_in_ZFC]
G
given_an_element [in FunctionsInZFC.Functions_in_ZFC]glueing_proof.glu_wd.gluD [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluC [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluB [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd.gluA [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof.glu_wd [in FunctionsInZFC.Functions_in_ZFC]
glueing_proof [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2B [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2.gd2A [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1b [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1.gd1a [in FunctionsInZFC.Functions_in_ZFC]
glueing_domain1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr2 [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof.gr1 [in FunctionsInZFC.Functions_in_ZFC]
glueing_relation_proof [in FunctionsInZFC.Functions_in_ZFC]
H
has_leq_0_implies_leq_1 [in FunctionsInZFC.Functions_in_ZFC]I
Intersection_section1.Intersection_section1_1 [in FunctionsInZFC.Functions_in_ZFC]Intersection_section1 [in FunctionsInZFC.Functions_in_ZFC]
intersection4 [in FunctionsInZFC.Functions_in_ZFC]
inv_eval_in_domain_proof [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof.cpb1 [in FunctionsInZFC.Functions_in_ZFC]
in_cartesian_bounded_proof [in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub_Zero_proof [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep2 [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof.ieieep1 [in FunctionsInZFC.Functions_in_ZFC]
its_empty_implies_equals_emptyset_proof [in FunctionsInZFC.Functions_in_ZFC]
N
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b.naturals_main_induction3bI [in FunctionsInZFC.Functions_in_ZFC]naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3b [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em.naturals_main_induction3a [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3.naturals_main_induction3em [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction3 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2c [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2b [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2.naturals_main_induction2a [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step.naturals_main_induction2 [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction_step [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof.naturals_inductionA1 [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_proof [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
neq_symm_proof [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero [in FunctionsInZFC.Functions_in_ZFC]
not_in_itself_Zero [in FunctionsInZFC.Functions_in_ZFC]
O
one_different_from_two [in FunctionsInZFC.Functions_in_ZFC]P
PAIR_proj_uni_proof [in FunctionsInZFC.Functions_in_ZFC]pair_proj2_proof [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_proof [in FunctionsInZFC.Functions_in_ZFC]
powerplus1 [in FunctionsInZFC.Functions_in_ZFC]
powerplus2 [in FunctionsInZFC.Functions_in_ZFC]
power0 [in FunctionsInZFC.Functions_in_ZFC]
power1 [in FunctionsInZFC.Functions_in_ZFC]
power2 [in FunctionsInZFC.Functions_in_ZFC]
power3 [in FunctionsInZFC.Functions_in_ZFC]
power4 [in FunctionsInZFC.Functions_in_ZFC]
power5 [in FunctionsInZFC.Functions_in_ZFC]
R
Range_th1_proof [in FunctionsInZFC.Functions_in_ZFC]Range_prop_bounded_proof.Range_prop_bounded_proof_1 [in FunctionsInZFC.Functions_in_ZFC]
Range_prop_bounded_proof [in FunctionsInZFC.Functions_in_ZFC]
relations_in_cartesian_proof [in FunctionsInZFC.Functions_in_ZFC]
relation_1 [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1b [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1.res_to_1a [in FunctionsInZFC.Functions_in_ZFC]
restricted_to_1 [in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_proof [in FunctionsInZFC.Functions_in_ZFC]
res_to_3 [in FunctionsInZFC.Functions_in_ZFC]
res_to_2 [in FunctionsInZFC.Functions_in_ZFC]
S
second_uniqueness_proof [in FunctionsInZFC.Functions_in_ZFC]second_has_geq_2_elements_proof.second_geq_2_a [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_proof [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_proof [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof.Singleton_th1_sub1 [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof.strictsub_next1 [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_proof [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof.strictsub_trans1a [in FunctionsInZFC.Functions_in_ZFC]
strictsub_trans1_proof [in FunctionsInZFC.Functions_in_ZFC]
subset_reflexive [in FunctionsInZFC.Functions_in_ZFC]
SUB_trans_proof [in FunctionsInZFC.Functions_in_ZFC]
T
total_and_pairs_1 [in FunctionsInZFC.Functions_in_ZFC]total_th4_proof [in FunctionsInZFC.Functions_in_ZFC]
total_th3_proof [in FunctionsInZFC.Functions_in_ZFC]
total_th2_proof [in FunctionsInZFC.Functions_in_ZFC]
total_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
U
Union_th1_proof [in FunctionsInZFC.Functions_in_ZFC]union_symm_proof [in FunctionsInZFC.Functions_in_ZFC]
union_refl_proof [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4b [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra.ut4a [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof.ut4contra [in FunctionsInZFC.Functions_in_ZFC]
union_th4_proof [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof.B_sub_V_proof1 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.B_sub_V_proof [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof.A_sub_V_proof1 [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof.A_sub_V_proof [in FunctionsInZFC.Functions_in_ZFC]
union_th3_proof [in FunctionsInZFC.Functions_in_ZFC]
union_th2_proof [in FunctionsInZFC.Functions_in_ZFC]
union_th1_proof [in FunctionsInZFC.Functions_in_ZFC]
W
well_def_1 [in FunctionsInZFC.Functions_in_ZFC]when_given_two_distinct_elements [in FunctionsInZFC.Functions_in_ZFC]
Z
Zero_element_of_NN_proof [in FunctionsInZFC.Functions_in_ZFC]zero_different_from_one [in FunctionsInZFC.Functions_in_ZFC]
Definition Index
A
A_in_next_A_Out [in FunctionsInZFC.Functions_in_ZFC]A_sub_next_A_Out [in FunctionsInZFC.Functions_in_ZFC]
a_pair_is_a_pair_Out [in FunctionsInZFC.Functions_in_ZFC]
A_sub_V_proof1_Out [in FunctionsInZFC.Functions_in_ZFC]
B
big_extensionality_Out [in FunctionsInZFC.Functions_in_ZFC]Bounded [in FunctionsInZFC.Functions_in_ZFC]
boundedsubprops1_Out [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
Bounded_NN_proof2_Out [in FunctionsInZFC.Functions_in_ZFC]
Bounded_subprops1_Out [in FunctionsInZFC.Functions_in_ZFC]
Bounded_CHOICE [in FunctionsInZFC.Functions_in_ZFC]
Bounded_th1_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
Bounded_By [in FunctionsInZFC.Functions_in_ZFC]
B_sub_V_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
b_in_Union_a [in FunctionsInZFC.Functions_in_ZFC]
C
Cartesian [in FunctionsInZFC.Functions_in_ZFC]Choose_an_element [in FunctionsInZFC.Functions_in_ZFC]
COMP [in FunctionsInZFC.Functions_in_ZFC]
Comp_INTERp [in FunctionsInZFC.Functions_in_ZFC]
Comp_INTER [in FunctionsInZFC.Functions_in_ZFC]
D
distinct_doubletons_have_geq_2_elements_Out [in FunctionsInZFC.Functions_in_ZFC]DOESNT_EXIST [in FunctionsInZFC.Functions_in_ZFC]
Domain [in FunctionsInZFC.Functions_in_ZFC]
Domain_prop [in FunctionsInZFC.Functions_in_ZFC]
Doubleton [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_2_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_uniqueness_1_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4b_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4a_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_sub2_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th4_sub1_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th3_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th2_Out [in FunctionsInZFC.Functions_in_ZFC]
doubleton_th1_Out [in FunctionsInZFC.Functions_in_ZFC]
E
Element_of_NN [in FunctionsInZFC.Functions_in_ZFC]EV [in FunctionsInZFC.Functions_in_ZFC]
EXISTS [in FunctionsInZFC.Functions_in_ZFC]
Extensionally_equivalent [in FunctionsInZFC.Functions_in_ZFC]
F
First [in FunctionsInZFC.Functions_in_ZFC]first_uniqueness_Out [in FunctionsInZFC.Functions_in_ZFC]
G
given_an_element_Out [in FunctionsInZFC.Functions_in_ZFC]H
has_geq_2_elements [in FunctionsInZFC.Functions_in_ZFC]has_leq_0_implies_leq_1_Out [in FunctionsInZFC.Functions_in_ZFC]
has_leq_1_elements [in FunctionsInZFC.Functions_in_ZFC]
has_geq_1_elements [in FunctionsInZFC.Functions_in_ZFC]
has_leq_0_elements [in FunctionsInZFC.Functions_in_ZFC]
I
Intersection [in FunctionsInZFC.Functions_in_ZFC]intersection [in FunctionsInZFC.Functions_in_ZFC]
IntersectionProp [in FunctionsInZFC.Functions_in_ZFC]
Intersection_Bounded [in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1_Out [in FunctionsInZFC.Functions_in_ZFC]
Intersection_section1_1_Out [in FunctionsInZFC.Functions_in_ZFC]
inverse_EV [in FunctionsInZFC.Functions_in_ZFC]
in_iff_strictsub_Zero_Out [in FunctionsInZFC.Functions_in_ZFC]
in_then_strictsub [in FunctionsInZFC.Functions_in_ZFC]
is_a_relation [in FunctionsInZFC.Functions_in_ZFC]
is_a_pair [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
Its_nonempty [in FunctionsInZFC.Functions_in_ZFC]
Its_empty [in FunctionsInZFC.Functions_in_ZFC]
N
Naturals [in FunctionsInZFC.Functions_in_ZFC]naturals_main_induction_step_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3em_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3b_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3bI_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction3a_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2c_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2b_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_main_induction2a_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_induction_nexts [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA_Out [in FunctionsInZFC.Functions_in_ZFC]
naturals_inductionA1_Out [in FunctionsInZFC.Functions_in_ZFC]
Naturals_th1_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
NEQ [in FunctionsInZFC.Functions_in_ZFC]
Next [in FunctionsInZFC.Functions_in_ZFC]
Nexts_element_of_NN_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
nothing_strictsub_Zero_Out [in FunctionsInZFC.Functions_in_ZFC]
not_in_itself_Zero_Out [in FunctionsInZFC.Functions_in_ZFC]
not_in_itself [in FunctionsInZFC.Functions_in_ZFC]
O
one_different_from_two_Out [in FunctionsInZFC.Functions_in_ZFC]P
PAIR [in FunctionsInZFC.Functions_in_ZFC]PAIR_proj_uni_Out [in FunctionsInZFC.Functions_in_ZFC]
pair_uniqueness_Out [in FunctionsInZFC.Functions_in_ZFC]
PowerPlus [in FunctionsInZFC.Functions_in_ZFC]
Powerset [in FunctionsInZFC.Functions_in_ZFC]
PowerTotal [in FunctionsInZFC.Functions_in_ZFC]
PR1 [in FunctionsInZFC.Functions_in_ZFC]
PR2 [in FunctionsInZFC.Functions_in_ZFC]
R
Range [in FunctionsInZFC.Functions_in_ZFC]Range_prop [in FunctionsInZFC.Functions_in_ZFC]
restricted_to [in FunctionsInZFC.Functions_in_ZFC]
restriction_bounded_Out [in FunctionsInZFC.Functions_in_ZFC]
S
Second [in FunctionsInZFC.Functions_in_ZFC]second_uniqueness_Out [in FunctionsInZFC.Functions_in_ZFC]
second_has_geq_2_elements_Out [in FunctionsInZFC.Functions_in_ZFC]
second_geq_2_a_Out [in FunctionsInZFC.Functions_in_ZFC]
Set_containing_NN [in FunctionsInZFC.Functions_in_ZFC]
Set_Of [in FunctionsInZFC.Functions_in_ZFC]
singletons_have_leq_1_elements_Out [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th2_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
Singleton_th1_sub1_Out [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next_Out [in FunctionsInZFC.Functions_in_ZFC]
strictsub_next1_Out [in FunctionsInZFC.Functions_in_ZFC]
SUB [in FunctionsInZFC.Functions_in_ZFC]
SUBPROP [in FunctionsInZFC.Functions_in_ZFC]
T
Total [in FunctionsInZFC.Functions_in_ZFC]U
Union [in FunctionsInZFC.Functions_in_ZFC]UnionPlus [in FunctionsInZFC.Functions_in_ZFC]
Union_intermediate [in FunctionsInZFC.Functions_in_ZFC]
union_th2_Out [in FunctionsInZFC.Functions_in_ZFC]
union_th1_Out [in FunctionsInZFC.Functions_in_ZFC]
W
well_definedness [in FunctionsInZFC.Functions_in_ZFC]when_given_two_distinct_elements_Out [in FunctionsInZFC.Functions_in_ZFC]
Z
Zero [in FunctionsInZFC.Functions_in_ZFC]Zero_element_of_NN_proof_Out [in FunctionsInZFC.Functions_in_ZFC]
zero_different_from_one_Out [in FunctionsInZFC.Functions_in_ZFC]
Record Index
C
Comp_prop [in FunctionsInZFC.Functions_in_ZFC]Comp_inter [in FunctionsInZFC.Functions_in_ZFC]
Contains_NN [in FunctionsInZFC.Functions_in_ZFC]
E
EQ [in FunctionsInZFC.Functions_in_ZFC]I
in_cartesian [in FunctionsInZFC.Functions_in_ZFC]is_a_function_on [in FunctionsInZFC.Functions_in_ZFC]
is_a_function [in FunctionsInZFC.Functions_in_ZFC]
N
naturals_main_ind_hyp [in FunctionsInZFC.Functions_in_ZFC]nested_IN [in FunctionsInZFC.Functions_in_ZFC]
P
pairwise_EQ [in FunctionsInZFC.Functions_in_ZFC]R
Restriction [in FunctionsInZFC.Functions_in_ZFC]S
StrictSUB [in FunctionsInZFC.Functions_in_ZFC]U
union_th3_property [in FunctionsInZFC.Functions_in_ZFC]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1757 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1102 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (311 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (161 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (121 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |