Theorem wl-ax12v2cl 37548

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

Theorem ax12v2 2182 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 2180 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 2735	. . 3 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝐴 ↔ 𝑦 = 𝐴))
2	1	cbvexvw 2038	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
3		ax12v 2181	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
4		eqeq2 2743	. . . . 5 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝑧 ↔ 𝑥 = 𝐴))
5	4	imbi1d 341	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜑)))
6	5	albidv 1921	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
7	6	imbi2d 340	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8	4, 7	imbi12d 344	. . . 4 ⊢ (𝑧 = 𝐴 → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
9	3, 8	mpbii 233	. . 3 ⊢ (𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
10	9	exlimiv 1931	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
11	2, 10	sylbir 235	1 ⊢ (∃𝑦 𝑦 = 𝐴 → (𝑥 = 𝐴 → (𝜑 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by: (None)