Theorem wl-ax12v2cl 38039

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

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

Theorem ax12v2 2221 expresses that two equal set variables cannot be distinguished by whatever complicated formula 𝜑 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 𝜑.

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 𝐴 is different from another, or distinct from a variable with type wff. So ax-12 2219 proper is out of reach: you cannot replace 𝑦 in ∀𝑦𝜑 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.)

Assertion

Ref	Expression
wl-ax12v2cl	⊢ (∃𝑦 𝑦 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem wl-ax12v2cl

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2773	. . 3 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝐴 ↔ 𝑦 = 𝐴))
2	1	cbvexvw 2064	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
3		ax12v 2220	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
4		eqeq2 2781	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝑧 ↔ 𝑥 = 𝐴))
5	4	imbi1d 344	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)))
6	5	albidv 1947	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
7	6	imbi2d 343	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8	4, 7	imbi12d 347	. . . 4 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
9	3, 8	mpbii 236	. . 3 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
10	9	exlimiv 1957	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
11	2, 10	sylbir 238	1 ⊢ (∃𝑦 𝑦 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))

Syntax hints:   → wi 4  ∀wal 1565   = wceq 1567  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by: (None)