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