Metamath Proof Explorer


Theorem elrnmpt1

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis rnmpt.1 𝐹 = ( 𝑥𝐴𝐵 )
Assertion elrnmpt1 ( ( 𝑥𝐴𝐵𝑉 ) → 𝐵 ∈ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 rnmpt.1 𝐹 = ( 𝑥𝐴𝐵 )
2 vex 𝑥 ∈ V
3 id ( 𝑥 = 𝑧𝑥 = 𝑧 )
4 csbeq1a ( 𝑥 = 𝑧𝐴 = 𝑧 / 𝑥 𝐴 )
5 3 4 eleq12d ( 𝑥 = 𝑧 → ( 𝑥𝐴𝑧 𝑧 / 𝑥 𝐴 ) )
6 csbeq1a ( 𝑥 = 𝑧𝐵 = 𝑧 / 𝑥 𝐵 )
7 6 biantrud ( 𝑥 = 𝑧 → ( 𝑧 𝑧 / 𝑥 𝐴 ↔ ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ) )
8 5 7 bitr2d ( 𝑥 = 𝑧 → ( ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ↔ 𝑥𝐴 ) )
9 8 equcoms ( 𝑧 = 𝑥 → ( ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ↔ 𝑥𝐴 ) )
10 2 9 spcev ( 𝑥𝐴 → ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) )
11 df-rex ( ∃ 𝑥𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ( 𝑥𝐴𝑦 = 𝐵 ) )
12 nfv 𝑧 ( 𝑥𝐴𝑦 = 𝐵 )
13 nfcsb1v 𝑥 𝑧 / 𝑥 𝐴
14 13 nfcri 𝑥 𝑧 𝑧 / 𝑥 𝐴
15 nfcsb1v 𝑥 𝑧 / 𝑥 𝐵
16 15 nfeq2 𝑥 𝑦 = 𝑧 / 𝑥 𝐵
17 14 16 nfan 𝑥 ( 𝑧 𝑧 / 𝑥 𝐴𝑦 = 𝑧 / 𝑥 𝐵 )
18 6 eqeq2d ( 𝑥 = 𝑧 → ( 𝑦 = 𝐵𝑦 = 𝑧 / 𝑥 𝐵 ) )
19 5 18 anbi12d ( 𝑥 = 𝑧 → ( ( 𝑥𝐴𝑦 = 𝐵 ) ↔ ( 𝑧 𝑧 / 𝑥 𝐴𝑦 = 𝑧 / 𝑥 𝐵 ) ) )
20 12 17 19 cbvexv1 ( ∃ 𝑥 ( 𝑥𝐴𝑦 = 𝐵 ) ↔ ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝑦 = 𝑧 / 𝑥 𝐵 ) )
21 11 20 bitri ( ∃ 𝑥𝐴 𝑦 = 𝐵 ↔ ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝑦 = 𝑧 / 𝑥 𝐵 ) )
22 eqeq1 ( 𝑦 = 𝐵 → ( 𝑦 = 𝑧 / 𝑥 𝐵𝐵 = 𝑧 / 𝑥 𝐵 ) )
23 22 anbi2d ( 𝑦 = 𝐵 → ( ( 𝑧 𝑧 / 𝑥 𝐴𝑦 = 𝑧 / 𝑥 𝐵 ) ↔ ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ) )
24 23 exbidv ( 𝑦 = 𝐵 → ( ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝑦 = 𝑧 / 𝑥 𝐵 ) ↔ ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ) )
25 21 24 syl5bb ( 𝑦 = 𝐵 → ( ∃ 𝑥𝐴 𝑦 = 𝐵 ↔ ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ) )
26 1 rnmpt ran 𝐹 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 }
27 25 26 elab2g ( 𝐵𝑉 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑧 ( 𝑧 𝑧 / 𝑥 𝐴𝐵 = 𝑧 / 𝑥 𝐵 ) ) )
28 10 27 syl5ibr ( 𝐵𝑉 → ( 𝑥𝐴𝐵 ∈ ran 𝐹 ) )
29 28 impcom ( ( 𝑥𝐴𝐵𝑉 ) → 𝐵 ∈ ran 𝐹 )