Metamath Proof Explorer


Theorem nfabdwOLD

Description: Obsolete version of nfabdw as of 23-Sep-2024. (Contributed by Mario Carneiro, 8-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses nfabdw.1 𝑦 𝜑
nfabdw.2 ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion nfabdwOLD ( 𝜑 𝑥 { 𝑦𝜓 } )

Proof

Step Hyp Ref Expression
1 nfabdw.1 𝑦 𝜑
2 nfabdw.2 ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 nfv 𝑧 𝜑
4 df-clab ( 𝑧 ∈ { 𝑦𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 )
5 1 2 alrimi ( 𝜑 → ∀ 𝑦𝑥 𝜓 )
6 nfa1 𝑦𝑦𝑥 𝜓
7 sb6 ( [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑧𝜓 ) )
8 7 a1i ( ∀ 𝑦𝑥 𝜓 → ( [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑧𝜓 ) ) )
9 7 biimpri ( ∀ 𝑦 ( 𝑦 = 𝑧𝜓 ) → [ 𝑧 / 𝑦 ] 𝜓 )
10 9 axc4i ( ∀ 𝑦 ( 𝑦 = 𝑧𝜓 ) → ∀ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 )
11 8 10 syl6bi ( ∀ 𝑦𝑥 𝜓 → ( [ 𝑧 / 𝑦 ] 𝜓 → ∀ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 ) )
12 6 11 nf5d ( ∀ 𝑦𝑥 𝜓 → Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 )
13 6 12 nfim1 𝑦 ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 )
14 sbequ12 ( 𝑦 = 𝑧 → ( 𝜓 ↔ [ 𝑧 / 𝑦 ] 𝜓 ) )
15 14 imbi2d ( 𝑦 = 𝑧 → ( ( ∀ 𝑦𝑥 𝜓𝜓 ) ↔ ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ) )
16 13 15 equsalv ( ∀ 𝑦 ( 𝑦 = 𝑧 → ( ∀ 𝑦𝑥 𝜓𝜓 ) ) ↔ ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) )
17 16 bicomi ( ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ( ∀ 𝑦𝑥 𝜓𝜓 ) ) )
18 nfv 𝑥 𝑦 = 𝑧
19 nfnf1 𝑥𝑥 𝜓
20 19 nfal 𝑥𝑦𝑥 𝜓
21 sp ( ∀ 𝑦𝑥 𝜓 → Ⅎ 𝑥 𝜓 )
22 20 21 nfim1 𝑥 ( ∀ 𝑦𝑥 𝜓𝜓 )
23 18 22 nfim 𝑥 ( 𝑦 = 𝑧 → ( ∀ 𝑦𝑥 𝜓𝜓 ) )
24 23 nfal 𝑥𝑦 ( 𝑦 = 𝑧 → ( ∀ 𝑦𝑥 𝜓𝜓 ) )
25 17 24 nfxfr 𝑥 ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 )
26 pm5.5 ( ∀ 𝑦𝑥 𝜓 → ( ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ↔ [ 𝑧 / 𝑦 ] 𝜓 ) )
27 20 26 nfbidf ( ∀ 𝑦𝑥 𝜓 → ( Ⅎ 𝑥 ( ∀ 𝑦𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ↔ Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 ) )
28 25 27 mpbii ( ∀ 𝑦𝑥 𝜓 → Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 )
29 5 28 syl ( 𝜑 → Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 )
30 4 29 nfxfrd ( 𝜑 → Ⅎ 𝑥 𝑧 ∈ { 𝑦𝜓 } )
31 3 30 nfcd ( 𝜑 𝑥 { 𝑦𝜓 } )