Theorem wl-ax12v2cl 38000

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

Theorem ax12v2 2214 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 2212 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 2766	. . 3 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝐴 ↔ 𝑦 = 𝐴))
2	1	cbvexvw 2057	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
3		ax12v 2213	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
4		eqeq2 2774	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝑧 ↔ 𝑥 = 𝐴))
5	4	imbi1d 343	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)))
6	5	albidv 1940	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
7	6	imbi2d 342	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8	4, 7	imbi12d 346	. . . 4 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
9	3, 8	mpbii 235	. . 3 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
10	9	exlimiv 1950	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
11	2, 10	sylbir 237	1 ⊢ (∃𝑦 𝑦 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))

Syntax hints:   → wi 4  ∀wal 1558   = wceq 1560  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by: (None)