Metamath Proof Explorer


Theorem invdisjrabw

Description: Version of invdisjrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion invdisjrabw DisjyAxB|C=y

Proof

Step Hyp Ref Expression
1 nfcv _xz
2 nfcv _xB
3 nfcsb1v _xz/xC
4 3 nfeq1 xz/xC=y
5 csbeq1a x=zC=z/xC
6 5 eqeq1d x=zC=yz/xC=y
7 1 2 4 6 elrabf zxB|C=yzBz/xC=y
8 simprr yAzBz/xC=yz/xC=y
9 7 8 sylan2b yAzxB|C=yz/xC=y
10 9 rgen2 yAzxB|C=yz/xC=y
11 invdisj yAzxB|C=yz/xC=yDisjyAxB|C=y
12 10 11 ax-mp DisjyAxB|C=y