Theorem dfich2bi 43689

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

Assertion

Ref	Expression
dfich2bi	⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑))

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

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem dfich2bi

Step	Hyp	Ref	Expression
1		nfa1 2154	. . 3 ⊢ Ⅎ𝑎∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
2		nfa2 2175	. . . . 5 ⊢ Ⅎ𝑏∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)
3		2sp 2184	. . . . . 6 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑))
4		sbcom2 2167	. . . . . 6 ⊢ ([𝑏 / 𝑥][𝑎 / 𝑦]𝜑 ↔ [𝑎 / 𝑦][𝑏 / 𝑥]𝜑)
5	3, 4	syl6bb 289	. . . . 5 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦][𝑏 / 𝑥]𝜑))
6	2, 5	sbbid 2245	. . . 4 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑥 / 𝑏][𝑎 / 𝑦][𝑏 / 𝑥]𝜑))
7		sbcom2 2167	. . . 4 ⊢ ([𝑥 / 𝑏][𝑎 / 𝑦][𝑏 / 𝑥]𝜑 ↔ [𝑎 / 𝑦][𝑥 / 𝑏][𝑏 / 𝑥]𝜑)
8	6, 7	syl6bb 289	. . 3 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦][𝑥 / 𝑏][𝑏 / 𝑥]𝜑))
9	1, 8	sbbid 2245	. 2 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑦 / 𝑎][𝑎 / 𝑦][𝑥 / 𝑏][𝑏 / 𝑥]𝜑))
10		sbco4 2283	. 2 ⊢ ([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑)
11		sbid2vw 2259	. . 3 ⊢ ([𝑦 / 𝑎][𝑎 / 𝑦][𝑥 / 𝑏][𝑏 / 𝑥]𝜑 ↔ [𝑥 / 𝑏][𝑏 / 𝑥]𝜑)
12		sbid2vw 2259	. . 3 ⊢ ([𝑥 / 𝑏][𝑏 / 𝑥]𝜑 ↔ 𝜑)
13	11, 12	bitri 277	. 2 ⊢ ([𝑦 / 𝑎][𝑎 / 𝑦][𝑥 / 𝑏][𝑏 / 𝑥]𝜑 ↔ 𝜑)
14	9, 10, 13	3bitr3g 315	1 ⊢ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1534  [wsb 2068

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

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

This theorem is referenced by:  dfich2OLD  43690