Metamath Proof Explorer


Theorem bnj23

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj23.1 B=xA|¬φ
Assertion bnj23 zB¬zRywAwRy[˙w/x]˙φ

Proof

Step Hyp Ref Expression
1 bnj23.1 B=xA|¬φ
2 sbcng wV[˙w/x]˙¬φ¬[˙w/x]˙φ
3 2 elv [˙w/x]˙¬φ¬[˙w/x]˙φ
4 1 eleq2i wBwxA|¬φ
5 nfcv _xA
6 5 elrabsf wxA|¬φwA[˙w/x]˙¬φ
7 4 6 bitri wBwA[˙w/x]˙¬φ
8 breq1 z=wzRywRy
9 8 notbid z=w¬zRy¬wRy
10 9 rspccv zB¬zRywB¬wRy
11 7 10 syl5bir zB¬zRywA[˙w/x]˙¬φ¬wRy
12 11 expdimp zB¬zRywA[˙w/x]˙¬φ¬wRy
13 3 12 syl5bir zB¬zRywA¬[˙w/x]˙φ¬wRy
14 13 con4d zB¬zRywAwRy[˙w/x]˙φ
15 14 ralrimiva zB¬zRywAwRy[˙w/x]˙φ