Theorem ac6sfi

Description: A version of ac6s for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009) (Proof shortened by Mario Carneiro, 29-Jan-2014)

	Ref	Expression
Hypothesis	ac6sfi.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ac6sfi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ac6sfi.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
2		raleq	⊢ ( 𝑢 = ∅ → ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
3		feq2	⊢ ( 𝑢 = ∅ → ( 𝑓 : 𝑢 ⟶ 𝐵 ↔ 𝑓 : ∅ ⟶ 𝐵 ) )
4		raleq	⊢ ( 𝑢 = ∅ → ( ∀ 𝑥 ∈ 𝑢 𝜓 ↔ ∀ 𝑥 ∈ ∅ 𝜓 ) )
5	3 4	anbi12d	⊢ ( 𝑢 = ∅ → ( ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) ) )
6	5	exbidv	⊢ ( 𝑢 = ∅ → ( ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) ) )
7	2 6	imbi12d	⊢ ( 𝑢 = ∅ → ( ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) ) ) )
8		raleq	⊢ ( 𝑢 = 𝑤 → ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
9		feq2	⊢ ( 𝑢 = 𝑤 → ( 𝑓 : 𝑢 ⟶ 𝐵 ↔ 𝑓 : 𝑤 ⟶ 𝐵 ) )
10		raleq	⊢ ( 𝑢 = 𝑤 → ( ∀ 𝑥 ∈ 𝑢 𝜓 ↔ ∀ 𝑥 ∈ 𝑤 𝜓 ) )
11	9 10	anbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) )
12	11	exbidv	⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) )
13	8 12	imbi12d	⊢ ( 𝑢 = 𝑤 → ( ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) ) )
14		raleq	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 ) )
15		feq2	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( 𝑓 : 𝑢 ⟶ 𝐵 ↔ 𝑓 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ) )
16		raleq	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ 𝑢 𝜓 ↔ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝜓 ) )
17	15 16	anbi12d	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ( 𝑓 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝜓 ) ) )
18	17	exbidv	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝜓 ) ) )
19		feq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ↔ 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ) )
20		fvex	⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
21	20 1	sbcie	⊢ ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ 𝜓 )
22		fveq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
23	22	sbceq1d	⊢ ( 𝑓 = 𝑔 → ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
24	21 23	bitr3id	⊢ ( 𝑓 = 𝑔 → ( 𝜓 ↔ [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
25	24	ralbidv	⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝜓 ↔ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
26	19 25	anbi12d	⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝜓 ) ↔ ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) )
27	26	cbvexvw	⊢ ( ∃ 𝑓 ( 𝑓 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝜓 ) ↔ ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
28	18 27	bitrdi	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) )
29	14 28	imbi12d	⊢ ( 𝑢 = ( 𝑤 ∪ { 𝑧 } ) → ( ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) )
30		raleq	⊢ ( 𝑢 = 𝐴 → ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
31		feq2	⊢ ( 𝑢 = 𝐴 → ( 𝑓 : 𝑢 ⟶ 𝐵 ↔ 𝑓 : 𝐴 ⟶ 𝐵 ) )
32		raleq	⊢ ( 𝑢 = 𝐴 → ( ∀ 𝑥 ∈ 𝑢 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
33	31 32	anbi12d	⊢ ( 𝑢 = 𝐴 → ( ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
34	33	exbidv	⊢ ( 𝑢 = 𝐴 → ( ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
35	30 34	imbi12d	⊢ ( 𝑢 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑢 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 𝜓 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) )
36		f0	⊢ ∅ : ∅ ⟶ 𝐵
37		0ex	⊢ ∅ ∈ V
38		ral0	⊢ ∀ 𝑥 ∈ ∅ 𝜓
39	38	biantru	⊢ ( 𝑓 : ∅ ⟶ 𝐵 ↔ ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) )
40		feq1	⊢ ( 𝑓 = ∅ → ( 𝑓 : ∅ ⟶ 𝐵 ↔ ∅ : ∅ ⟶ 𝐵 ) )
41	39 40	bitr3id	⊢ ( 𝑓 = ∅ → ( ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) ↔ ∅ : ∅ ⟶ 𝐵 ) )
42	37 41	spcev	⊢ ( ∅ : ∅ ⟶ 𝐵 → ∃ 𝑓 ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) )
43	36 42	mp1i	⊢ ( ∀ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : ∅ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ∅ 𝜓 ) )
44		ssun1	⊢ 𝑤 ⊆ ( 𝑤 ∪ { 𝑧 } )
45		ssralv	⊢ ( 𝑤 ⊆ ( 𝑤 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
46	44 45	ax-mp	⊢ ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 )
47	46	imim1i	⊢ ( ( ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) )
48		ssun2	⊢ { 𝑧 } ⊆ ( 𝑤 ∪ { 𝑧 } )
49		ssralv	⊢ ( { 𝑧 } ⊆ ( 𝑤 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ 𝐵 𝜑 ) )
50	48 49	ax-mp	⊢ ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ 𝐵 𝜑 )
51		ralsnsg	⊢ ( 𝑧 ∈ V → ( ∀ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ 𝐵 𝜑 ↔ [ 𝑧 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ) )
52	51	elv	⊢ ( ∀ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ 𝐵 𝜑 ↔ [ 𝑧 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 )
53		sbcrex	⊢ ( [ 𝑧 / 𝑥 ] ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
54	52 53	bitri	⊢ ( ∀ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
55	50 54	sylib	⊢ ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
56		nfv	⊢ Ⅎ 𝑦 ¬ 𝑧 ∈ 𝑤
57		nfv	⊢ Ⅎ 𝑦 ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 )
58		nfv	⊢ Ⅎ 𝑦 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵
59		nfcv	⊢ Ⅎ 𝑦 ( 𝑤 ∪ { 𝑧 } )
60		nfsbc1v	⊢ Ⅎ 𝑦 [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑
61	59 60	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑
62	58 61	nfan	⊢ Ⅎ 𝑦 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
63	62	nfex	⊢ Ⅎ 𝑦 ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
64	57 63	nfim	⊢ Ⅎ 𝑦 ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
65		simprl	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → 𝑓 : 𝑤 ⟶ 𝐵 )
66		vex	⊢ 𝑧 ∈ V
67		vex	⊢ 𝑦 ∈ V
68	66 67	f1osn	⊢ { ⟨ 𝑧 , 𝑦 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑦 }
69		f1of	⊢ ( { ⟨ 𝑧 , 𝑦 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑦 } → { ⟨ 𝑧 , 𝑦 ⟩ } : { 𝑧 } ⟶ { 𝑦 } )
70	68 69	mp1i	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → { ⟨ 𝑧 , 𝑦 ⟩ } : { 𝑧 } ⟶ { 𝑦 } )
71		simpl2	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → 𝑦 ∈ 𝐵 )
72	71	snssd	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → { 𝑦 } ⊆ 𝐵 )
73	70 72	fssd	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → { ⟨ 𝑧 , 𝑦 ⟩ } : { 𝑧 } ⟶ 𝐵 )
74		simpl1	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ¬ 𝑧 ∈ 𝑤 )
75		disjsn	⊢ ( ( 𝑤 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑤 )
76	74 75	sylibr	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( 𝑤 ∩ { 𝑧 } ) = ∅ )
77	65 73 76	fun2d	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 )
78		simprr	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ∀ 𝑥 ∈ 𝑤 𝜓 )
79		eleq1a	⊢ ( 𝑥 ∈ 𝑤 → ( 𝑧 = 𝑥 → 𝑧 ∈ 𝑤 ) )
80	79	necon3bd	⊢ ( 𝑥 ∈ 𝑤 → ( ¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥 ) )
81	80	impcom	⊢ ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 ≠ 𝑥 )
82		fvunsn	⊢ ( 𝑧 ≠ 𝑥 → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
83		dfsbcq	⊢ ( ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) → ( [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
84	83 21	bitr2di	⊢ ( ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) → ( 𝜓 ↔ [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
85	81 82 84	3syl	⊢ ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤 ) → ( 𝜓 ↔ [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
86	85	ralbidva	⊢ ( ¬ 𝑧 ∈ 𝑤 → ( ∀ 𝑥 ∈ 𝑤 𝜓 ↔ ∀ 𝑥 ∈ 𝑤 [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
87	74 86	syl	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( ∀ 𝑥 ∈ 𝑤 𝜓 ↔ ∀ 𝑥 ∈ 𝑤 [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
88	78 87	mpbid	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ∀ 𝑥 ∈ 𝑤 [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 )
89		simpl3	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → [ 𝑧 / 𝑥 ] 𝜑 )
90		ffun	⊢ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 → Fun ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) )
91		ssun2	⊢ { ⟨ 𝑧 , 𝑦 ⟩ } ⊆ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } )
92		vsnid	⊢ 𝑧 ∈ { 𝑧 }
93	67	dmsnop	⊢ dom { ⟨ 𝑧 , 𝑦 ⟩ } = { 𝑧 }
94	92 93	eleqtrri	⊢ 𝑧 ∈ dom { ⟨ 𝑧 , 𝑦 ⟩ }
95		funssfv	⊢ ( ( Fun ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ∧ { ⟨ 𝑧 , 𝑦 ⟩ } ⊆ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ∧ 𝑧 ∈ dom { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) )
96	91 94 95	mp3an23	⊢ ( Fun ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) )
97	77 90 96	3syl	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) = ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) )
98	66 67	fvsn	⊢ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) = 𝑦
99	97 98	eqtr2di	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) )
100		ralsnsg	⊢ ( 𝑧 ∈ V → ( ∀ 𝑥 ∈ { 𝑧 } 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
101	100	elv	⊢ ( ∀ 𝑥 ∈ { 𝑧 } 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
102		elsni	⊢ ( 𝑥 ∈ { 𝑧 } → 𝑥 = 𝑧 )
103	102	fveq2d	⊢ ( 𝑥 ∈ { 𝑧 } → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) )
104	103	eqeq2d	⊢ ( 𝑥 ∈ { 𝑧 } → ( 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) ↔ 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) ) )
105	104	biimparc	⊢ ( ( 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) )
106		sbceq1a	⊢ ( 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) → ( 𝜑 ↔ [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
107	105 106	syl	⊢ ( ( 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) ∧ 𝑥 ∈ { 𝑧 } ) → ( 𝜑 ↔ [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
108	107	ralbidva	⊢ ( 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) → ( ∀ 𝑥 ∈ { 𝑧 } 𝜑 ↔ ∀ 𝑥 ∈ { 𝑧 } [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
109	101 108	bitr3id	⊢ ( 𝑦 = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑧 ) → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ∈ { 𝑧 } [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
110	99 109	syl	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ∈ { 𝑧 } [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
111	89 110	mpbid	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ∀ 𝑥 ∈ { 𝑧 } [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 )
112		ralun	⊢ ( ( ∀ 𝑥 ∈ 𝑤 [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ∧ ∀ 𝑥 ∈ { 𝑧 } [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 )
113	88 111 112	syl2anc	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 )
114		vex	⊢ 𝑓 ∈ V
115		snex	⊢ { ⟨ 𝑧 , 𝑦 ⟩ } ∈ V
116	114 115	unex	⊢ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ∈ V
117		feq1	⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ↔ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ) )
118		fveq1	⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( 𝑔 ‘ 𝑥 ) = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) )
119	118	sbceq1d	⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
120	119	ralbidv	⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
121	117 120	anbi12d	⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) → ( ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ↔ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) )
122	116 121	spcev	⊢ ( ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑦 ⟩ } ) ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
123	77 113 122	syl2anc	⊢ ( ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ∧ ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
124	123	ex	⊢ ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) → ( ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) )
125	124	exlimdv	⊢ ( ( ¬ 𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) )
126	125	3exp	⊢ ( ¬ 𝑧 ∈ 𝑤 → ( 𝑦 ∈ 𝐵 → ( [ 𝑧 / 𝑥 ] 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) ) )
127	56 64 126	rexlimd	⊢ ( ¬ 𝑧 ∈ 𝑤 → ( ∃ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) )
128	55 127	syl5	⊢ ( ¬ 𝑧 ∈ 𝑤 → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) )
129	128	a2d	⊢ ( ¬ 𝑧 ∈ 𝑤 → ( ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) )
130	47 129	syl5	⊢ ( ¬ 𝑧 ∈ 𝑤 → ( ( ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) )
131	130	adantl	⊢ ( ( 𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤 ) → ( ( ∀ 𝑥 ∈ 𝑤 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑤 𝜓 ) ) → ( ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑔 ( 𝑔 : ( 𝑤 ∪ { 𝑧 } ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑤 ∪ { 𝑧 } ) [ ( 𝑔 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ) )
132	7 13 29 35 43 131	findcard2s	⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
133	132	imp	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )