Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcrext Structured version   Unicode version

Theorem sbcrext 3248
 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.)
Assertion
Ref Expression
sbcrext
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   (,)   ()

Proof of Theorem sbcrext
StepHypRef Expression
1 sbcng 3207 . . . . 5
21adantr 453 . . . 4
3 sbcralt 3246 . . . . . 6
4 nfnfc1 2581 . . . . . . . . 9
5 id 21 . . . . . . . . . 10
6 nfcvd 2579 . . . . . . . . . 10
75, 6nfeld 2593 . . . . . . . . 9
84, 7nfan1 1847 . . . . . . . 8
9 sbcng 3207 . . . . . . . . 9
109adantl 454 . . . . . . . 8
118, 10ralbid 2729 . . . . . . 7
1211ancoms 441 . . . . . 6
133, 12bitrd 246 . . . . 5
1413notbid 287 . . . 4
152, 14bitrd 246 . . 3
16 dfrex2 2724 . . . 4
1716sbcbii 3225 . . 3
18 dfrex2 2724 . . 3
1915, 17, 183bitr4g 281 . 2
20 sbcex 3176 . . . . 5
2120con3i 130 . . . 4