Metamath Proof Explorer


Theorem bnj941

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj941.1 G=fnC
Assertion bnj941 CVp=sucnfFnnGFnp

Proof

Step Hyp Ref Expression
1 bnj941.1 G=fnC
2 opeq2 C=ifCVCnC=nifCVC
3 2 sneqd C=ifCVCnC=nifCVC
4 3 uneq2d C=ifCVCfnC=fnifCVC
5 1 4 eqtrid C=ifCVCG=fnifCVC
6 5 fneq1d C=ifCVCGFnpfnifCVCFnp
7 6 imbi2d C=ifCVCp=sucnfFnnGFnpp=sucnfFnnfnifCVCFnp
8 eqid fnifCVC=fnifCVC
9 0ex V
10 9 elimel ifCVCV
11 8 10 bnj927 p=sucnfFnnfnifCVCFnp
12 7 11 dedth CVp=sucnfFnnGFnp