Metamath Proof Explorer

Theorem imaeqexov

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

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

Proof

Step Hyp Ref Expression
1 imaeqexov.1 ⊢ ( 𝑥 = ( 𝑦 𝐹 𝑧 ) → ( 𝜑 ↔ 𝜓 ) )
2 df-rex ⊢ ( ∃ 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ∧ 𝜑 ) )
3 ovelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ) )
4 3 anbi1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ) )
5 r19.41v ⊢ ( ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ( ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) )
6 5 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) )
7 r19.41v ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) )
8 6 7 bitr2i ⊢ ( ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) )
9 4 8 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ) )
10 9 exbidv ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ) )
11 rexcom4 ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) )
12 rexcom4 ⊢ ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑥 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) )
13 ovex ⊢ ( 𝑦 𝐹 𝑧 ) ∈ V
14 13 1 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ 𝜓 )
15 14 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑥 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝐶 𝜓 )
16 12 15 bitr3i ⊢ ( ∃ 𝑥 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝐶 𝜓 )
17 16 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜓 )
18 11 17 bitr3i ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 ( 𝑥 = ( 𝑦 𝐹 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜓 )
19 10 18 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜓 ) )
20 2 19 bitrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝜓 ) )