Metamath Proof Explorer


Theorem sbcrext

Description: Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016) (Revised by NM, 18-Aug-2018) (Proof shortened by JJ, 7-Jul-2021)

Ref Expression
Assertion sbcrext _yA[˙A/x]˙yBφyB[˙A/x]˙φ

Proof

Step Hyp Ref Expression
1 sbcex [˙A/x]˙yBφAV
2 1 a1i _yA[˙A/x]˙yBφAV
3 nfnfc1 y_yA
4 id _yA_yA
5 nfcvd _yA_yV
6 4 5 nfeld _yAyAV
7 sbcex [˙A/x]˙φAV
8 7 2a1i _yAyB[˙A/x]˙φAV
9 3 6 8 rexlimd2 _yAyB[˙A/x]˙φAV
10 sbcng AV[˙A/x]˙¬yB¬φ¬[˙A/x]˙yB¬φ
11 10 adantl _yAAV[˙A/x]˙¬yB¬φ¬[˙A/x]˙yB¬φ
12 sbcralt AV_yA[˙A/x]˙yB¬φyB[˙A/x]˙¬φ
13 12 ancoms _yAAV[˙A/x]˙yB¬φyB[˙A/x]˙¬φ
14 3 6 nfan1 y_yAAV
15 sbcng AV[˙A/x]˙¬φ¬[˙A/x]˙φ
16 15 adantl _yAAV[˙A/x]˙¬φ¬[˙A/x]˙φ
17 14 16 ralbid _yAAVyB[˙A/x]˙¬φyB¬[˙A/x]˙φ
18 13 17 bitrd _yAAV[˙A/x]˙yB¬φyB¬[˙A/x]˙φ
19 18 notbid _yAAV¬[˙A/x]˙yB¬φ¬yB¬[˙A/x]˙φ
20 11 19 bitrd _yAAV[˙A/x]˙¬yB¬φ¬yB¬[˙A/x]˙φ
21 dfrex2 yBφ¬yB¬φ
22 21 sbcbii [˙A/x]˙yBφ[˙A/x]˙¬yB¬φ
23 dfrex2 yB[˙A/x]˙φ¬yB¬[˙A/x]˙φ
24 20 22 23 3bitr4g _yAAV[˙A/x]˙yBφyB[˙A/x]˙φ
25 24 ex _yAAV[˙A/x]˙yBφyB[˙A/x]˙φ
26 2 9 25 pm5.21ndd _yA[˙A/x]˙yBφyB[˙A/x]˙φ