This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imaeqsexvOLD

Description: Obsolete version of rexima as of 14-Aug-2025. Duplicate version of rexima . (Contributed by Scott Fenton, 27-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 imaeqsexvOLD.1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
2 df-rex ⊢ ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ∧ 𝜑 ) )
3 fvelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
4 3 anbi1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ) )
5 4 exbidv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ) )
6 2 5 bitrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ) )
7 rexcom4 ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) )
8 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑦 ) )
9 8 anbi1i ⊢ ( ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ∧ 𝜑 ) )
10 9 exbii ⊢ ( ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ∧ 𝜑 ) )
11 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
12 11 1 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ∧ 𝜑 ) ↔ 𝜓 )
13 10 12 bitri ⊢ ( ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ 𝜓 )
14 13 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 𝜓 )
15 r19.41v ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) )
16 15 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) )
17 7 14 16 3bitr3ri ⊢ ( ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 𝜓 )
18 6 17 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) )