This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfcsbw

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 12-Oct-2016) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

Ref Expression
Hypotheses nfcsbw.1 
|- F/_ x A
nfcsbw.2 
|- F/_ x B
Assertion nfcsbw 
|- F/_ x [_ A / y ]_ B

Proof

Step Hyp Ref Expression
1 nfcsbw.1 
 |-  F/_ x A
2 nfcsbw.2 
 |-  F/_ x B
3 df-csb 
 |-  [_ A / y ]_ B = { z | [. A / y ]. z e. B }
4 nftru 
 |-  F/ z T.
5 nftru 
 |-  F/ y T.
6 1 a1i 
 |-  ( T. -> F/_ x A )
7 2 a1i 
 |-  ( T. -> F/_ x B )
8 7 nfcrd 
 |-  ( T. -> F/ x z e. B )
9 5 6 8 nfsbcdw 
 |-  ( T. -> F/ x [. A / y ]. z e. B )
10 4 9 nfabdw 
 |-  ( T. -> F/_ x { z | [. A / y ]. z e. B } )
11 3 10 nfcxfrd 
 |-  ( T. -> F/_ x [_ A / y ]_ B )
12 11 mptru 
 |-  F/_ x [_ A / y ]_ B