Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑦 = 𝐴 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐴 ) ) |
2 |
|
eleq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) ) |
3 |
2
|
rabbidv |
⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) |
4 |
3
|
inteqd |
⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) |
5 |
1 4
|
eqeq12d |
⊢ ( 𝑦 = 𝐴 → ( ( rank ‘ 𝑦 ) = ∩ { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ↔ ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) ) |
6 |
|
vex |
⊢ 𝑦 ∈ V |
7 |
6
|
rankval |
⊢ ( rank ‘ 𝑦 ) = ∩ { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } |
8 |
5 7
|
vtoclg |
⊢ ( 𝐴 ∈ 𝑉 → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) |