Metamath Proof Explorer


Theorem rdgsucmpt2

Description: This version of rdgsucmpt avoids the not-free hypothesis of rdgsucmptf by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses rdgsucmpt2.1 F = rec x V C A
rdgsucmpt2.2 y = x E = C
rdgsucmpt2.3 y = F B E = D
Assertion rdgsucmpt2 B On D V F suc B = D

Proof

Step Hyp Ref Expression
1 rdgsucmpt2.1 F = rec x V C A
2 rdgsucmpt2.2 y = x E = C
3 rdgsucmpt2.3 y = F B E = D
4 nfcv _ y A
5 nfcv _ y B
6 nfcv _ y D
7 2 cbvmptv y V E = x V C
8 rdgeq1 y V E = x V C rec y V E A = rec x V C A
9 7 8 ax-mp rec y V E A = rec x V C A
10 1 9 eqtr4i F = rec y V E A
11 4 5 6 10 3 rdgsucmptf B On D V F suc B = D