Metamath Proof Explorer


Theorem elabrex

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014)

Ref Expression
Hypothesis elabrex.1 𝐵 ∈ V
Assertion elabrex ( 𝑥𝐴𝐵 ∈ { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )

Proof

Step Hyp Ref Expression
1 elabrex.1 𝐵 ∈ V
2 tru
3 csbeq1a ( 𝑥 = 𝑧𝐵 = 𝑧 / 𝑥 𝐵 )
4 3 equcoms ( 𝑧 = 𝑥𝐵 = 𝑧 / 𝑥 𝐵 )
5 trud ( 𝑧 = 𝑥 → ⊤ )
6 4 5 2thd ( 𝑧 = 𝑥 → ( 𝐵 = 𝑧 / 𝑥 𝐵 ↔ ⊤ ) )
7 6 rspcev ( ( 𝑥𝐴 ∧ ⊤ ) → ∃ 𝑧𝐴 𝐵 = 𝑧 / 𝑥 𝐵 )
8 2 7 mpan2 ( 𝑥𝐴 → ∃ 𝑧𝐴 𝐵 = 𝑧 / 𝑥 𝐵 )
9 eqeq1 ( 𝑦 = 𝐵 → ( 𝑦 = 𝑧 / 𝑥 𝐵𝐵 = 𝑧 / 𝑥 𝐵 ) )
10 9 rexbidv ( 𝑦 = 𝐵 → ( ∃ 𝑧𝐴 𝑦 = 𝑧 / 𝑥 𝐵 ↔ ∃ 𝑧𝐴 𝐵 = 𝑧 / 𝑥 𝐵 ) )
11 1 10 elab ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑧𝐴 𝑦 = 𝑧 / 𝑥 𝐵 } ↔ ∃ 𝑧𝐴 𝐵 = 𝑧 / 𝑥 𝐵 )
12 8 11 sylibr ( 𝑥𝐴𝐵 ∈ { 𝑦 ∣ ∃ 𝑧𝐴 𝑦 = 𝑧 / 𝑥 𝐵 } )
13 nfv 𝑧 𝑦 = 𝐵
14 nfcsb1v 𝑥 𝑧 / 𝑥 𝐵
15 14 nfeq2 𝑥 𝑦 = 𝑧 / 𝑥 𝐵
16 3 eqeq2d ( 𝑥 = 𝑧 → ( 𝑦 = 𝐵𝑦 = 𝑧 / 𝑥 𝐵 ) )
17 13 15 16 cbvrexw ( ∃ 𝑥𝐴 𝑦 = 𝐵 ↔ ∃ 𝑧𝐴 𝑦 = 𝑧 / 𝑥 𝐵 )
18 17 abbii { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } = { 𝑦 ∣ ∃ 𝑧𝐴 𝑦 = 𝑧 / 𝑥 𝐵 }
19 12 18 eleqtrrdi ( 𝑥𝐴𝐵 ∈ { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )