This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
Assertion bnj23 ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → [ 𝑤 / 𝑥 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 bnj23.1 ⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
2 sbcng ⊢ ( 𝑤 ∈ V → ( [ 𝑤 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑤 / 𝑥 ] 𝜑 ) )
3 2 elv ⊢ ( [ 𝑤 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑤 / 𝑥 ] 𝜑 )
4 1 eleq2i ⊢ ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } )
5 nfcv ⊢ Ⅎ 𝑥 𝐴
6 5 elrabsf ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] ¬ 𝜑 ) )
7 4 6 bitri ⊢ ( 𝑤 ∈ 𝐵 ↔ ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] ¬ 𝜑 ) )
8 breq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑤 𝑅 𝑦 ) )
9 8 notbid ⊢ ( 𝑧 = 𝑤 → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑤 𝑅 𝑦 ) )
10 9 rspccv ⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 → ( 𝑤 ∈ 𝐵 → ¬ 𝑤 𝑅 𝑦 ) )
11 7 10 biimtrrid ⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 → ( ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] ¬ 𝜑 ) → ¬ 𝑤 𝑅 𝑦 ) )
12 11 expdimp ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 ∧ 𝑤 ∈ 𝐴 ) → ( [ 𝑤 / 𝑥 ] ¬ 𝜑 → ¬ 𝑤 𝑅 𝑦 ) )
13 3 12 biimtrrid ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ [ 𝑤 / 𝑥 ] 𝜑 → ¬ 𝑤 𝑅 𝑦 ) )
14 13 con4d ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑦 → [ 𝑤 / 𝑥 ] 𝜑 ) )
15 14 ralrimiva ⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → [ 𝑤 / 𝑥 ] 𝜑 ) )