Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
⊢ ( 𝐴 = 𝐶 → ( 𝐴 ∈ V ↔ 𝐶 ∈ V ) ) |
2 |
|
oveq2 |
⊢ ( 𝐴 = 𝐶 → ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) = ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐶 ) ) |
3 |
|
raleq |
⊢ ( 𝐴 = 𝐶 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐶 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ) |
4 |
3
|
exbidv |
⊢ ( 𝐴 = 𝐶 → ( ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑔 ∀ 𝑦 ∈ 𝐶 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ) |
5 |
2 4
|
raleqbidv |
⊢ ( 𝐴 = 𝐶 → ( ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐶 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐶 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ) |
6 |
1 5
|
anbi12d |
⊢ ( 𝐴 = 𝐶 → ( ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐶 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐶 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐶 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ) ) |
7 |
6
|
abbidv |
⊢ ( 𝐴 = 𝐶 → { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) } = { 𝑥 ∣ ( 𝐶 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐶 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐶 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) } ) |
8 |
|
df-acn |
⊢ AC 𝐴 = { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) } |
9 |
|
df-acn |
⊢ AC 𝐶 = { 𝑥 ∣ ( 𝐶 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐶 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐶 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) } |
10 |
7 8 9
|
3eqtr4g |
⊢ ( 𝐴 = 𝐶 → AC 𝐴 = AC 𝐶 ) |