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

Metamath Proof Explorer

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 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )