There are two very different kinds of question here:
What is logic exactly? ... What is "proof"? What is "truth"?
All good questions. But famously they do not have sharp, determinate, clear, uncontentious answers. Indeed, they are characteristically philosophical questions (that fall into the purview of what is often called "philosophical logic").
Of course, a technical logic text will introduce e.g. a sharp, technical, notion of a proof-in-a-given-formal-system (the fine print can be significantly different in different texts). But what is the relation between (1) the everyday notion of mathematical proof and (2) various notions of proof-in-a-given-formal-system which aim to model mathematical proof? This is up for (philosophical) debate. Similarly for the notion of truth, and indeed for the notion of a logic.
A "rigorous logic text" is therefore not the best place, really, to look for the discussion of the philosophical questions here. For those questions are (as it were) standing back from details in those rigorous texts and asking more general, philosophical, questions about them.
Please recommend me a good precise logic textbook.
Still, if you do want pointers to formal logic textbooks then there are a lot of suggestions, at various levels, on various areas of logic, in the Guide you can find at http://www.logicmatters.net/tyl
No but you can say:
Let P be (x ∈ A)
Let Q be (x ∈ B)
A ⊆ B ≡ ∀x, P → Q
⊆ is for sets
→ is for propositions
Note: You cannot say the same for A ⊂ B
Why?
Let A be {1}
Let B be {1}
Let P be (x ∈ A)
Let Q be (x ∈ B)
A ⊂ B is false.
∀x, P → Q is true.
Therefore A ⊂ B cannot be equivalent to ∀x, P → Q
Best Answer
In classical logic, the logical connectives are truth-functional, i.e. defined by their truth-table.
With them, we may easily verify that the two formulae :
are equivalent.
If you are not "at ease" with this result, you are not alone: in Intuitionsitic Logic this result is not provable.
In effect, this logic does not "agree" on the truth-functional definition of the connectives.
In the context of "classical logic" the best "intuition I can suggest you is to reflect how the $\to$ connective is used in mathematical reasoning by way of modus ponens rule of inference.
We "apply" it asserting the premises :$A \to B$ and $A$.
The first assertion excludes the case when $A$ is true and $B$ false, while the second assertion excludes the two cases where $A$ is false.
Thus, the truth-table fo $\to$ leaves us only one possibility : $B$ true, and this is what we need in order to conclude the proof.
The same happens with the "disjunction version" of the same rule :
In words : if we know that at least one between $\lnot A$ and $B$ holds and if we know that $A$ holds (i.e. $\lnot A$ does not), we have to conclude that $B$ must hold.