Theorem wl-ax12v2cl 38152

Description: The class version of ax12v2 2215, 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 2214 is a specialization of ax12v2 2215. So any proof using ax12v 2214 will still hold if ax12v2 2215 is used instead.

Theorem ax12v2 2215 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 2213 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 2767	. . 3 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝐴 ↔ 𝑦 = 𝐴))
2	1	cbvexvw 2067	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
3		ax12v 2214	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
4		eqeq2 2775	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝑧 ↔ 𝑥 = 𝐴))
5	4	imbi1d 344	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)))
6	5	albidv 1950	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
7	6	imbi2d 343	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8	4, 7	imbi12d 347	. . . 4 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
9	3, 8	mpbii 236	. . 3 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
10	9	exlimiv 1960	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
11	2, 10	sylbir 238	1 ⊢ (∃𝑦 𝑦 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))

Syntax hints:   → wi 4  ∀wal 1568   = wceq 1570  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by: (None)