This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acneq

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

Ref Expression
Assertion acneq ( 𝐴 = 𝐶 → AC 𝐴 = AC 𝐶 )

Proof

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 𝐶 )