Theorem ralcom4OLD

Description: Obsolete version of ralcom4 as of 31-Oct-2024. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ralcom4OLD	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		19.21v	⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) )
2	1	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3	2	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
4		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
5	3 4	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) )
7		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
8	7	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
9	5 6 8	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )