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 = x ∈ A | ¬ φ
Assertion bnj23 ⊢ ∀ z ∈ B ¬ z R y → ∀ w ∈ A w R y → [˙w / x]˙ φ

Proof

Step Hyp Ref Expression
1 bnj23.1 ⊢ B = x ∈ A | ¬ φ
2 sbcng ⊢ w ∈ V → [˙w / x]˙ ¬ φ ↔ ¬ [˙w / x]˙ φ
3 2 elv ⊢ [˙w / x]˙ ¬ φ ↔ ¬ [˙w / x]˙ φ
4 1 eleq2i ⊢ w ∈ B ↔ w ∈ x ∈ A | ¬ φ
5 nfcv ⊢ Ⅎ _ x A
6 5 elrabsf ⊢ w ∈ x ∈ A | ¬ φ ↔ w ∈ A ∧ [˙w / x]˙ ¬ φ
7 4 6 bitri ⊢ w ∈ B ↔ w ∈ A ∧ [˙w / x]˙ ¬ φ
8 breq1 ⊢ z = w → z R y ↔ w R y
9 8 notbid ⊢ z = w → ¬ z R y ↔ ¬ w R y
10 9 rspccv ⊢ ∀ z ∈ B ¬ z R y → w ∈ B → ¬ w R y
11 7 10 syl5bir ⊢ ∀ z ∈ B ¬ z R y → w ∈ A ∧ [˙w / x]˙ ¬ φ → ¬ w R y
12 11 expdimp ⊢ ∀ z ∈ B ¬ z R y ∧ w ∈ A → [˙w / x]˙ ¬ φ → ¬ w R y
13 3 12 syl5bir ⊢ ∀ z ∈ B ¬ z R y ∧ w ∈ A → ¬ [˙w / x]˙ φ → ¬ w R y
14 13 con4d ⊢ ∀ z ∈ B ¬ z R y ∧ w ∈ A → w R y → [˙w / x]˙ φ
15 14 ralrimiva ⊢ ∀ z ∈ B ¬ z R y → ∀ w ∈ A w R y → [˙w / x]˙ φ