Metamath Proof Explorer


Theorem cbvrexcsf

Description: A more general version of cbvrexf that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (Proof shortened by Mario Carneiro, 7-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses cbvralcsf.1 _yA
cbvralcsf.2 _xB
cbvralcsf.3 yφ
cbvralcsf.4 xψ
cbvralcsf.5 x=yA=B
cbvralcsf.6 x=yφψ
Assertion cbvrexcsf xAφyBψ

Proof

Step Hyp Ref Expression
1 cbvralcsf.1 _yA
2 cbvralcsf.2 _xB
3 cbvralcsf.3 yφ
4 cbvralcsf.4 xψ
5 cbvralcsf.5 x=yA=B
6 cbvralcsf.6 x=yφψ
7 3 nfn y¬φ
8 4 nfn x¬ψ
9 6 notbid x=y¬φ¬ψ
10 1 2 7 8 5 9 cbvralcsf xA¬φyB¬ψ
11 10 notbii ¬xA¬φ¬yB¬ψ
12 dfrex2 xAφ¬xA¬φ
13 dfrex2 yBψ¬yB¬ψ
14 11 12 13 3bitr4i xAφyBψ