Metamath Proof Explorer


Theorem bj-ax12ig

Description: A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i . (Contributed by BJ, 19-Dec-2020)

Ref Expression
Hypotheses bj-ax12ig.1
|- ( ph -> ( ps <-> ch ) )
bj-ax12ig.2
|- ( ph -> ( ch -> A. x ch ) )
Assertion bj-ax12ig
|- ( ph -> ( ps -> A. x ( ph -> ps ) ) )

Proof

Step Hyp Ref Expression
1 bj-ax12ig.1
 |-  ( ph -> ( ps <-> ch ) )
2 bj-ax12ig.2
 |-  ( ph -> ( ch -> A. x ch ) )
3 1 pm5.32i
 |-  ( ( ph /\ ps ) <-> ( ph /\ ch ) )
4 2 imp
 |-  ( ( ph /\ ch ) -> A. x ch )
5 1 biimprcd
 |-  ( ch -> ( ph -> ps ) )
6 4 5 sylg
 |-  ( ( ph /\ ch ) -> A. x ( ph -> ps ) )
7 3 6 sylbi
 |-  ( ( ph /\ ps ) -> A. x ( ph -> ps ) )
8 7 ex
 |-  ( ph -> ( ps -> A. x ( ph -> ps ) ) )