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 y φ
nfabdw.2 φ x ψ
Assertion nfabdwOLD φ _ x y | ψ

Proof

Step Hyp Ref Expression
1 nfabdw.1 y φ
2 nfabdw.2 φ x ψ
3 nfv z φ
4 df-clab z y | ψ z y ψ
5 1 2 alrimi φ y x ψ
6 nfa1 y y x ψ
7 sb6 z y ψ y y = z ψ
8 7 a1i y x ψ z y ψ y y = z ψ
9 7 biimpri y y = z ψ z y ψ
10 9 axc4i y y = z ψ y z y ψ
11 8 10 syl6bi y x ψ z y ψ y z y ψ
12 6 11 nf5d y x ψ y z y ψ
13 6 12 nfim1 y y x ψ z y ψ
14 sbequ12 y = z ψ z y ψ
15 14 imbi2d y = z y x ψ ψ y x ψ z y ψ
16 13 15 equsalv y y = z y x ψ ψ y x ψ z y ψ
17 16 bicomi y x ψ z y ψ y y = z y x ψ ψ
18 nfv x y = z
19 nfnf1 x x ψ
20 19 nfal x y x ψ
21 sp y x ψ x ψ
22 20 21 nfim1 x y x ψ ψ
23 18 22 nfim x y = z y x ψ ψ
24 23 nfal x y y = z y x ψ ψ
25 17 24 nfxfr x y x ψ z y ψ
26 pm5.5 y x ψ y x ψ z y ψ z y ψ
27 20 26 nfbidf y x ψ x y x ψ z y ψ x z y ψ
28 25 27 mpbii y x ψ x z y ψ
29 5 28 syl φ x z y ψ
30 4 29 nfxfrd φ x z y | ψ
31 3 30 nfcd φ _ x y | ψ