Metamath Proof Explorer


Theorem sbbibvv

Description: Reversal of substitution. (Contributed by AV, 6-Aug-2023)

Ref Expression
Assertion sbbibvv
|- ( A. y ( [ y / x ] ph <-> ps ) <-> A. x ( ph <-> [ x / y ] ps ) )

Proof

Step Hyp Ref Expression
1 nfv
 |-  F/ y ph
2 nfv
 |-  F/ x ps
3 1 2 sbbib
 |-  ( A. y ( [ y / x ] ph <-> ps ) <-> A. x ( ph <-> [ x / y ] ps ) )