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 ) )