Metamath Proof Explorer

Theorem imaeqalov

Description: Substitute an operation value into a universal quantifier over an image. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypothesis imaeqexov.1 ⊢ ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion imaeqalov ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ) )

Proof

Step Hyp Ref Expression
1 imaeqexov.1 ⊢ ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → ( 𝜑 ↔ 𝜓 ) )
2 df-ral ⊢ ( ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) → 𝜑 ) )
3 ovelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ) )
4 3 imbi1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ) )
5 4 albidv ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) → 𝜑 ) ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ) )
6 2 5 bitrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) 𝜑 ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ) )
7 ralcom4 ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
8 r19.23v ⊢ ( ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
9 8 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
10 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
11 9 10 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
12 11 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
13 7 12 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
14 ralcom4 ⊢ ( ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) )
15 ovex ⊢ ( 𝑦 𝐹 𝑧 ) ∈ V
16 15 1 ceqsalv ⊢ ( ∀ 𝑥 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ 𝜓 )
17 16 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐶 𝜓 )
18 14 17 bitr3i ⊢ ( ∀ 𝑥 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐶 𝜓 )
19 18 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∀ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 )
20 13 19 bitr3i ⊢ ( ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 )
21 6 20 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ) )