Metamath Proof Explorer


Theorem ralxfrd

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by NM, 15-Aug-2014) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

Ref Expression
Hypotheses ralxfrd.1 φyCAB
ralxfrd.2 φxByCx=A
ralxfrd.3 φx=Aψχ
Assertion ralxfrd φxBψyCχ

Proof

Step Hyp Ref Expression
1 ralxfrd.1 φyCAB
2 ralxfrd.2 φxByCx=A
3 ralxfrd.3 φx=Aψχ
4 3 adantlr φyCx=Aψχ
5 1 4 rspcdv φyCxBψχ
6 5 ralrimdva φxBψyCχ
7 r19.29 yCχyCx=AyCχx=A
8 3 exbiri φx=Aχψ
9 8 impcomd φχx=Aψ
10 9 rexlimdvw φyCχx=Aψ
11 7 10 syl5 φyCχyCx=Aψ
12 11 adantr φxByCχyCx=Aψ
13 2 12 mpan2d φxByCχψ
14 13 ralrimdva φyCχxBψ
15 6 14 impbid φxBψyCχ