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 |
⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) |