Theorem dfich2OLD 43690

Description: Obsolete version of dfich2 43687 as of 18-Sep-2023. Alternate definition of the propery of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. (Contributed by AV, 6-Aug-2023.) (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
dfich2OLD	⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))

Distinct variable groups:   𝑎,𝑏,𝜑   𝑥,𝑎,𝑦,𝑏

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem dfich2OLD

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ich 43680	. 2 ⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑))
2		nfv 1914	. . . 4 ⊢ Ⅎ𝑎∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑)
3		nfv 1914	. . . . 5 ⊢ Ⅎ𝑏∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑)
4		dfich2ai 43688	. . . . 5 ⊢ (∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
5	3, 4	alrimi 2212	. . . 4 ⊢ (∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
6	2, 5	alrimi 2212	. . 3 ⊢ (∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) → ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
7		nfs1v 2159	. . . . . . 7 ⊢ Ⅎ𝑥[𝑎 / 𝑥][𝑏 / 𝑦]𝜑
8		nfs1v 2159	. . . . . . 7 ⊢ Ⅎ𝑥[𝑏 / 𝑥][𝑎 / 𝑦]𝜑
9	7, 8	nfbi 1903	. . . . . 6 ⊢ Ⅎ𝑥([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
10	9	nfal 2341	. . . . 5 ⊢ Ⅎ𝑥∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
11	10	nfal 2341	. . . 4 ⊢ Ⅎ𝑥∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
12		nfs1v 2159	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑏 / 𝑦]𝜑
13	12	nfsb 2564	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑎 / 𝑥][𝑏 / 𝑦]𝜑
14		nfs1v 2159	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑎 / 𝑦]𝜑
15	14	nfsb 2564	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑏 / 𝑥][𝑎 / 𝑦]𝜑
16	13, 15	nfbi 1903	. . . . . . 7 ⊢ Ⅎ𝑦([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
17	16	nfal 2341	. . . . . 6 ⊢ Ⅎ𝑦∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
18	17	nfal 2341	. . . . 5 ⊢ Ⅎ𝑦∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
19		dfich2bi 43689	. . . . 5 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑))
20	18, 19	alrimi 2212	. . . 4 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑))
21	11, 20	alrimi 2212	. . 3 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑))
22	6, 21	impbii 211	. 2 ⊢ (∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
23	1, 22	bitri 277	1 ⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))

Syntax hints:   ↔ wb 208  ∀wal 1534  [wsb 2068  [wich 43679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-10 2144  ax-11 2160  ax-12 2176  ax-13 2389

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-ich 43680

This theorem is referenced by: (None)