elsetpreimafv - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elsetpreimafv		Structured version Visualization version GIF version

Theorem elsetpreimafv 46788

Description: An element of the class 𝑃 of all preimages of function values. (Contributed by AV, 8-Mar-2024.)

**Hypothesis**
Ref	Expression
setpreimafvex.p	⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (^◡𝐹 “ {(𝐹‘𝑥)})}

**Assertion**
Ref	Expression
elsetpreimafv	⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}))

Distinct variable groups: 𝑥,𝐴,𝑧 𝑥,𝐹,𝑧 𝑥,𝑆,𝑧 Allowed substitution hints: 𝑃(𝑥,𝑧)

**Proof of Theorem elsetpreimafv**
Step	Hyp	Ref	Expression
1		setpreimafvex.p	. . 3 ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (^◡𝐹 “ {(𝐹‘𝑥)})}
2	1	elsetpreimafvb 46787	. 2 ⊢ (𝑆 ∈ 𝑃 → (𝑆 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐴 𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)})))
3	2	ibi 266	1 ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 {cab 2702 ∃wrex 3060 {csn 4624 ^◡ccnv 5671 “ cima 5675 ‘cfv 6543

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696

This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rex 3061

This theorem is referenced by: elsetpreimafvssdm 46789 fvelsetpreimafv 46790 elsetpreimafvbi 46794 imasetpreimafvbijlemfo 46808

	
		OSZAR »