x ∈ F  ⇔ {x} ⊂ F ⇔ (∃y ∈ E, x=y∧y ∈ F) ⇔ (∀y ∈ E, x=y⇒y ∈ F) 
x ∈ F  ⇒ ((∀y ∈ F, A(y))⇒A(x)⇒∃y ∈ F, A(y)) 
F ⊂ {x}  ⇔ (∀y ∈ F, x=y) ⇒ ((∃y ∈ F, A(y))⇒A(x)⇒(∀y ∈ F, A(y))) 
F={x}  ⇔ (x ∈ F∧∀y ∈ F, x=y) ⇔ (∀y ∈ E, y ∈ F ⇔ x=y) 
(∃x∈E, A(x)) ⇔ (F ≠ ∅)  ⇔ (∃x∈F, 1) ⇔ (∃x∈E, {x} ⊂ F) 
(∃2x∈E, A(x)) ⇔ (∃2: F)  ⇔ (∃x,y ∈ F, x ≠ y) ⇔ (∃x,y ∈ E, A(x)∧A(y)∧x ≠ y) 
(!x∈E, A(x)) ⇔ (!:F)  ⇔ ¬(∃2: F) ⇔ (∀x,y ∈ F, x=y) ⇔ ∀x∈F, F ⊂ {x} 
(∃!x∈E, A(x)) ⇔ (∃!: F)  ⇔ (∃x∈F, F ⊂ {x}) ⇔ (∃x∈E, F={x}) 
F ⊂ {x}  ⇒∀y∈F, F ⊂ {y} ⇔ (!:F) 
(∃!:F)  ⇔ (F ≠ ∅∧!: F) 
F ≠ ∅  ⇒ ((∀y∈F, B(y)) ⇒ (∃y∈F, B(y))) 
( !: F)  ⇒ ((∃y∈F, B(y)) ⇒ (∀y∈F, B(y))) 
F={x}  ⇒ ((∃y∈F, B(y)) ⇔ B(x) ⇔ ∀y∈F, B(y)) 
(B? x:y) = (y,x)_{B} = ϵ{z∈{x,y}B ? z=x : z=y}
so that for any predicate A we have A(B? x:y) ⇔ (B? A(x):A(y)). All paraoperators other than connectives but with at least a Boolean argument, are naturally expressed as composed of the conditional operator with operators, or the conditional connective with predicates, which is why they did not need an explicit presence in the language of a theory.
Set theory and Foundations of Mathematics 

1.
First
foundations of mathematics 

2. Set theory (continued)  
2.1. Tuples, families 2.2. Boolean operators on families of sets 2.3. Products, graphs and composition ⇦ 2.4. Uniqueness quantifiers, functional graphs 
⇨ 2.5. The powerset
axiom 2.6. Injectivity and inversion 2.7. Properties of binary relations on a set ; ordered sets 2.8. Canonical bijections 2.9. Equivalence relations and partitions 2.10. Axiom of choice 2.11. Notion of Galois connection 
