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