Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
⊢ ( 𝐴 ∈ 𝑉 ▶ 𝐴 ∈ 𝑉 ) |
2 |
|
sbcel12 |
⊢ ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) |
3 |
2
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
4 |
1 3
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
5 |
|
csbconstg |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 = 〈 𝑤 , 𝑦 〉 ) |
6 |
1 5
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 = 〈 𝑤 , 𝑦 〉 ) |
7 |
|
eleq1 |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 = 〈 𝑤 , 𝑦 〉 → ( ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
8 |
6 7
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ ( ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
9 |
|
bibi1 |
⊢ ( ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) |
10 |
9
|
biimprd |
⊢ ( ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) |
11 |
4 8 10
|
e11 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
12 |
11
|
gen11 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ∀ 𝑤 ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
13 |
|
exbi |
⊢ ( ∀ 𝑤 ( [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
14 |
12 13
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
15 |
|
sbcex2 |
⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ) |
16 |
15
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ) ) |
17 |
16
|
bicomd |
⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ) ) |
18 |
1 17
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ) ) |
19 |
|
bitr3 |
⊢ ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ) → ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) |
20 |
19
|
com12 |
⊢ ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) |
21 |
14 18 20
|
e11 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
22 |
21
|
gen11 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
23 |
|
abbi |
⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) |
24 |
23
|
biimpi |
⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 ↔ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) |
25 |
22 24
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) |
26 |
|
csbab |
⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } |
27 |
26
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ) |
28 |
1 27
|
e1a |
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ) |
29 |
|
eqeq2 |
⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ↔ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) |
30 |
29
|
biimpd |
⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) |
31 |
25 28 30
|
e11 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) |
32 |
|
dfrn3 |
⊢ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } |
33 |
32
|
ax-gen |
⊢ ∀ 𝑥 ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } |
34 |
|
csbeq2 |
⊢ ( ∀ 𝑥 ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ) |
35 |
34
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ) ) |
36 |
1 33 35
|
e10 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ) |
37 |
|
eqeq2 |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } ↔ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) |
38 |
37
|
biimpd |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) |
39 |
31 36 38
|
e11 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) |
40 |
|
dfrn3 |
⊢ ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } |
41 |
|
eqeq2 |
⊢ ( ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) |
42 |
41
|
biimprcd |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 〈 𝑤 , 𝑦 〉 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) |
43 |
39 40 42
|
e10 |
⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) |
44 |
43
|
in1 |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ran 𝐵 = ran ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) |