Theorem wl-ax12v2cl 38209

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

Theorem ax12v2 2218 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 2216 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 2769	. . 3 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝐴 ↔ 𝑦 = 𝐴))
2	1	cbvexvw 2070	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
3		ax12v 2217	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
4		eqeq2 2777	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝑧 ↔ 𝑥 = 𝐴))
5	4	imbi1d 344	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)))
6	5	albidv 1953	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
7	6	imbi2d 343	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8	4, 7	imbi12d 347	. . . 4 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
9	3, 8	mpbii 236	. . 3 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
10	9	exlimiv 1963	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
11	2, 10	sylbir 238	1 ⊢ (∃𝑦 𝑦 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   = wceq 1570  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by: (None)