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	$⊢ x = y F z \to (φ \leftrightarrow ψ)$
	Assertion	imaeqexov	$⊢ (F Fn A \land B \times C \subseteq A) \to (\exists x \in F [B \times C] φ \leftrightarrow \exists y \in B \exists z \in C ψ)$

Proof

Step	Hyp	Ref	Expression
1		imaeqexov.1	$⊢ x = y F z \to (φ \leftrightarrow ψ)$
2		df-rex	$⊢ \exists x \in F [B \times C] φ \leftrightarrow \exists x (x \in F [B \times C] \land φ)$
3		ovelimab	$⊢ (F Fn A \land B \times C \subseteq A) \to (x \in F [B \times C] \leftrightarrow \exists y \in B \exists z \in C x = y F z)$
4	3	anbi1d	$⊢ (F Fn A \land B \times C \subseteq A) \to ((x \in F [B \times C] \land φ) \leftrightarrow (\exists y \in B \exists z \in C x = y F z \land φ))$
5		r19.41v	$⊢ \exists z \in C (x = y F z \land φ) \leftrightarrow (\exists z \in C x = y F z \land φ)$
6	5	rexbii	$⊢ \exists y \in B \exists z \in C (x = y F z \land φ) \leftrightarrow \exists y \in B (\exists z \in C x = y F z \land φ)$
7		r19.41v	$⊢ \exists y \in B (\exists z \in C x = y F z \land φ) \leftrightarrow (\exists y \in B \exists z \in C x = y F z \land φ)$
8	6 7	bitr2i	$⊢ (\exists y \in B \exists z \in C x = y F z \land φ) \leftrightarrow \exists y \in B \exists z \in C (x = y F z \land φ)$
9	4 8	bitrdi	$⊢ (F Fn A \land B \times C \subseteq A) \to ((x \in F [B \times C] \land φ) \leftrightarrow \exists y \in B \exists z \in C (x = y F z \land φ))$
10	9	exbidv	$⊢ (F Fn A \land B \times C \subseteq A) \to (\exists x (x \in F [B \times C] \land φ) \leftrightarrow \exists x \exists y \in B \exists z \in C (x = y F z \land φ))$
11		rexcom4	$⊢ \exists y \in B \exists x \exists z \in C (x = y F z \land φ) \leftrightarrow \exists x \exists y \in B \exists z \in C (x = y F z \land φ)$
12		rexcom4	$⊢ \exists z \in C \exists x (x = y F z \land φ) \leftrightarrow \exists x \exists z \in C (x = y F z \land φ)$
13		ovex	$⊢ y F z \in V$
14	13 1	ceqsexv	$⊢ \exists x (x = y F z \land φ) \leftrightarrow ψ$
15	14	rexbii	$⊢ \exists z \in C \exists x (x = y F z \land φ) \leftrightarrow \exists z \in C ψ$
16	12 15	bitr3i	$⊢ \exists x \exists z \in C (x = y F z \land φ) \leftrightarrow \exists z \in C ψ$
17	16	rexbii	$⊢ \exists y \in B \exists x \exists z \in C (x = y F z \land φ) \leftrightarrow \exists y \in B \exists z \in C ψ$
18	11 17	bitr3i	$⊢ \exists x \exists y \in B \exists z \in C (x = y F z \land φ) \leftrightarrow \exists y \in B \exists z \in C ψ$
19	10 18	bitrdi	$⊢ (F Fn A \land B \times C \subseteq A) \to (\exists x (x \in F [B \times C] \land φ) \leftrightarrow \exists y \in B \exists z \in C ψ)$
20	2 19	bitrid	$⊢ (F Fn A \land B \times C \subseteq A) \to (\exists x \in F [B \times C] φ \leftrightarrow \exists y \in B \exists z \in C ψ)$

Metamath Proof Explorer

Theorem imaeqexov

Proof