Step |
Hyp |
Ref |
Expression |
1 |
|
eleq2 |
⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝐵 ) ) |
2 |
|
fveq2 |
⊢ ( 𝑦 = 𝐵 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐵 ) ) |
3 |
2
|
eleq2d |
⊢ ( 𝑦 = 𝐵 → ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) ) |
4 |
1 3
|
imbi12d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑦 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) ) ) |
5 |
|
vex |
⊢ 𝑦 ∈ V |
6 |
5
|
rankel |
⊢ ( 𝐴 ∈ 𝑦 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝑦 ) ) |
7 |
4 6
|
vtoclg |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) ) |
8 |
7
|
imp |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) |