How can I prove that two ways of expressing that curve lies on the surface are equivalent. Simplified 1D case.

Question

Question. 1D case. How to prove that $\forall y \forall t [B(y) \impliedby x(t)=y]$ is equivalent to $\forall t \exists y[B(y) \land y=x(t)]$?

Relevance.

I) 3D case. I see two ways of expressing that a curve lies on a surface. I want to write a formal proof that both are equivalent.

1. First way of expressing that a curve lies on a surface is to say that parametric curve $x(t)=x \land y(t)=y \land z(t)=z$ lies on surface $A(x,y,z)=0$ is: $\forall t [A(x(t),y(t),z(t))=0]$
2. The second expression that says that the curve lies on the surface. Set of all points of parametric curve is $\exists t [x(t)=x \land y(t)=y \land z(t)=z]$. We need to say that set of all (x,y,z) of curve is a subset of all surface pints (x,y,z), that is: $\forall x\forall y \forall z [A(x,y,z)=0 \impliedby \exists t [x(t)=x \land y(t)=y \land z(t)=z]]$

So $\forall t [A(x(t),y(t),z(t))=0]$ should be equivalent with $\forall x\forall y \forall z [A(x,y,z)=0 \impliedby \exists t [x(t)=x \land y(t)=y \land z(t)=z]]$ I am not asking to answer on it is here only to understand my reasoning.

II) 2D case. Last question looked too complicated, so I want to start by proving simpler case. It is much simpler to reason about 2D surface and 2D curve inside it. Simpler question would be. Prove that $\forall x \forall y \exists t [A(x, y)<0 \impliedby x(t)=x \land y(t)=y]$ is equivalent with $\forall t [A(x(t), y(t))<0 ]$. I am not asking to answer on it, it is here only to understand my reasoning.

Example: Imagine some curve that lies completely in circle $x^2+y^2<4$. It should be so that if you plug parametric equation of that curve, for example $x=2sin(t)$, $y=2cos(t)$, you should obtain valid equation. If we chose for example x^2+y^2=5 ($x=5sin(t)$, $y=5cos(t)$) into $x^2+y^2<4$ will won't get valid equation.

III)1D case. We can simplify this question further, and it is question I am asking, that is 1D case. $\forall y [A(y)<0 \impliedby \exists t [x(t)=y]]$ is equivalent to $\forall t [A(x(t))<0]$?

We can generalize it even further: $\forall y [B(y) \impliedby \exists t [x(t)=y]]$ is equivalent to $\forall t [B(x(t))<0]$? It can be prove that it is equivalent to formula in "Question" section.

My attempt to solve 1D case question.

My strategy. I was able to prove that $\forall t[A(x(t))<0]$ is equivalent with $\forall t \exists y[A(y)<0\land x(t)=y]$ I attempted to prove my question by using reductio ad absurdum. That means that I need to deduce contradiction in the end of the proof. Also I am grasping that definition of function might be employed here.

Update.:

1. I found an error. At the beginning question was as follows. How to prove that $\forall y \exists t [A(y)<0 \impliedby x(t)=y]$ implies $\forall t \exists y[A(y)<0 \land y=x(t)]$? I didn't noticed that I used false rule that $P \impliedby \exists xQ(x)$ is equivalent with $\exists x[P \impliedby Q(x)]$. Right rule is $P \impliedby \exists xQ(x)$ is equivalent with $\forall x[P\impliedby Q(x)]$. Also I made 1D case more general.

P.S.: I am chemist, so things that are obvious to mathematicians might not be obvious to me. So I prefer proofs. Proof is sequence of formulas where each of them is an axiom or hypothesis, or derived from previous steps by inference rules. I prefer Fitch notation. It is very good if the proof comes from a book or publication. If you are using axioms other than thous that are in Fitch system please give reference to book, that can be comprehended by chemist. Please use Occam razor. I don't know how to write set theoretic proofs, although I thought myself predicate logic.

Answer 1

Here is a proof of 1D case, that is $\forall y \forall t [B(y) \impliedby x(t)=y]$ implies $\forall t \exists y[B(y) \land y= x(t)]$. I am sorry the way my proof looks. I didn't find a way how to input nice looking Fitch proof here, all internet tools doesn't support all need. 1D case.

1. |_$\forall y \forall t [B(y) \impliedby x(t)=y]$, hyp
2. | |_$\exists t \forall y[\lnot[B(y)] \land y\neq x(t)]$, hyp
3. | |t|_$\forall y[\lnot[B(y)] \lor y\neq x(t)]$, hyp
4. | | |$\forall y \forall t [B(y) \lor x(t)\neq y]$, 1 reit, rep def
5. | | |y|$\lnot[B(y)] \lor y\neq x(t)$ , 3 reit; u q elim
6. | | | |$ \forall t [B(y) \lor x(t)\neq y]$, 4 reit; u q elim
7. | | | |$B(y) \lor x(t)\neq y$ , 6 u q elim
8. | | | | |_$B(y)$. hyp
9. | | | | | $\lnot[B(y)] \lor y\neq x(t)$, 5, reit
10. | | | | | $y\neq x(t)$, 8,9 mtp
11. | | | | $y\neq x(t)$, 7,8-10, dis elim
12. | | $\exists t \forall y [y\neq x(t)]$, 5-11 u q int; 3-11, e q elim
13. | | $\lnot \forall t \exists y [y= x(t)]$, negation of quantifiers
14. | | $\forall t \exists y [x(t)= y]]$, because x(t) is a function.
15. | |$p \land \lnot p$, 14,15, neg elim
16. | $\lnot \exists t \forall y[\lnot[B(y)] \land y\neq x(t)]$, 2-16, reductio ad absurdum
17. | $\forall t \exists y[B(y) \land y= x(t)]$, 17, negation of quantifiers

Here is proof of that $\forall y \forall t [B(y) \impliedby x(t)=y]$ is implied by $\forall t \exists y[B(y) \land y= x(t)]$.

1. |_$\forall t \exists y[B(y) \land y=x(t)]$
2. |y| |_$\exists t [x(t)=y]$
3. | |t|_$x(t)=y$
4. | | |$\forall t \exists y[B(y)\land y=x(t)]$
5. | | |$\exists y[B(y)\land y=x(t)]$
6. | | |z|_$B(z)\land z=x(t)$
7. | | | |$B(z)$
8. | | | |$z=x(t)$
9. | | | |$B(x(t))$
10. | | | $B(x(t))$
11. | | | $B(y)$
12. | | $B(y)$
13. | |$B(y) \impliedby \exists t[x(t)=y]$
14. | |$B(y) \lor \lnot \exists t[x(t)=y]$
15. | ||_$\lnot \exists t[x(t)=y]$
16. | | |$ \forall t[x(t)\neq y]$
17. | | |t|$ x(t)\neq y$
18. | | | |$B(y) \lor x(t)\neq y$
19. | | | $\forall t [B(y) \lor x(t)\neq y]$
20. | | |_$B(y)$
21. | | |t|$B(y)$
22. | | | |$B(y)\lor x(t) \neq y$
23. | | | $\forall t [B(y)\lor x(t) \neq y]$
24. | | $\forall t [B(y)\lor x(t) \neq y]$
25. | $\forall y\forall t [B(y)\lor x(t) \neq y]$

3D case. It is possible to prove 3D case using 1D case proof where variables are substituted to vectors and parametric curve is replaced to vector function. To construct this proof it is needed to generalize natural deduction rules to arbitrary vectors. Proof is very similar to 1D case proof.