Description: Obsolete version of nfra2w as of 24-Sep-2024. (Contributed by Alan Sare, 31-Dec-2011) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfra2wOLD | |- F/ y A. x e. A A. y e. B ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv | |- F/_ y A |
|
| 2 | nfra1 | |- F/ y A. y e. B ph |
|
| 3 | 1 2 | nfralw | |- F/ y A. x e. A A. y e. B ph |