Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | abbii.1 | |
|
Assertion | abbii | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbii.1 | |
|
2 | abbi | |
|
3 | 2 1 | mpg | |