Theorem wl-ax12v2cl

Description: The class version of ax12v2 , where the set variable y is replaced with the class variable A . This is possible if A is known to be a set, expressed by the antecedent.

Theorem ax12v is a specialization of ax12v2 . So any proof using ax12v will still hold if ax12v2 is used instead.

Theorem ax12v2 expresses that two equal set variables cannot be distinguished by whatever complicated formula ph if one is replaced with the other in it. This theorem states a similar result for a class variable known to be a set: All sets equal to the class variable behave the same if they replace the class variable in ph .

Most axioms in FOL containing an equation correspond to a theorem where a class variable known to be a set replaces a set variable in the formula. Some exceptions cannot be avoided: The set variable must nowhere be bound. And it is not possible to state a distinct variable condition where a class A is different from another, or distinct from a variable with type wff. So ax-12 proper is out of reach: you cannot replace y in A. y ph with a class variable.

But where such limitations are not violated, the proof of the FOL theorem should carry over to a version where a class variable, known to be set, appears instead of a set variable. (Contributed by Wolf Lammen, 8-Aug-2020)

	Ref	Expression
Assertion	wl-ax12v2cl	$$⊢\exists yy=A\to \left(x=A\to \left(\phi \to \forall x\left(x=A\to \phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢z=y\to \left(z=A\leftrightarrow y=A\right)$$
2	1	cbvexvw	$$⊢\exists zz=A\leftrightarrow \exists yy=A$$
3		ax12v	$$⊢x=z\to \left(\phi \to \forall x\left(x=z\to \phi \right)\right)$$
4		eqeq2	$$⊢z=A\to \left(x=z\leftrightarrow x=A\right)$$
5	4	imbi1d	$$⊢z=A\to \left(\left(x=z\to \phi \right)\leftrightarrow \left(x=A\to \phi \right)\right)$$
6	5	albidv	$$⊢z=A\to \left(\forall x\left(x=z\to \phi \right)\leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
7	6	imbi2d	$$⊢z=A\to \left(\left(\phi \to \forall x\left(x=z\to \phi \right)\right)\leftrightarrow \left(\phi \to \forall x\left(x=A\to \phi \right)\right)\right)$$
8	4 7	imbi12d	$$⊢z=A\to \left(\left(x=z\to \left(\phi \to \forall x\left(x=z\to \phi \right)\right)\right)\leftrightarrow \left(x=A\to \left(\phi \to \forall x\left(x=A\to \phi \right)\right)\right)\right)$$
9	3 8	mpbii	$$⊢z=A\to \left(x=A\to \left(\phi \to \forall x\left(x=A\to \phi \right)\right)\right)$$
10	9	exlimiv	$$⊢\exists zz=A\to \left(x=A\to \left(\phi \to \forall x\left(x=A\to \phi \right)\right)\right)$$
11	2 10	sylbir	$$⊢\exists yy=A\to \left(x=A\to \left(\phi \to \forall x\left(x=A\to \phi \right)\right)\right)$$