Metamath Proof Explorer

Theorem acneq

Description: Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acneq ⊢ A = C → AC _ A = AC _ C

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ A = C → A ∈ V ↔ C ∈ V
2 oveq2 ⊢ A = C → 𝒫 x ∖ ∅ A = 𝒫 x ∖ ∅ C
3 raleq ⊢ A = C → ∀ y ∈ A g ⁡ y ∈ f ⁡ y ↔ ∀ y ∈ C g ⁡ y ∈ f ⁡ y
4 3 exbidv ⊢ A = C → ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y ↔ ∃ g ∀ y ∈ C g ⁡ y ∈ f ⁡ y
5 2 4 raleqbidv ⊢ A = C → ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y ↔ ∀ f ∈ 𝒫 x ∖ ∅ C ∃ g ∀ y ∈ C g ⁡ y ∈ f ⁡ y
6 1 5 anbi12d ⊢ A = C → A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y ↔ C ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ C ∃ g ∀ y ∈ C g ⁡ y ∈ f ⁡ y
7 6 abbidv ⊢ A = C → x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y = x | C ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ C ∃ g ∀ y ∈ C g ⁡ y ∈ f ⁡ y
8 df-acn ⊢ AC _ A = x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
9 df-acn ⊢ AC _ C = x | C ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ C ∃ g ∀ y ∈ C g ⁡ y ∈ f ⁡ y
10 7 8 9 3eqtr4g ⊢ A = C → AC _ A = AC _ C