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	syl5bir	⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 → ( ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] ¬ 𝜑 ) → ¬ 𝑤 𝑅 𝑦 ) )
12	11	expdimp	⊢ ( ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 ∧ 𝑤 ∈ 𝐴 ) → ( [ 𝑤 / 𝑥 ] ¬ 𝜑 → ¬ 𝑤 𝑅 𝑦 ) )
13	3 12	syl5bir	⊢ ( ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ [ 𝑤 / 𝑥 ] 𝜑 → ¬ 𝑤 𝑅 𝑦 ) )
14	13	con4d	⊢ ( ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑦 → [ 𝑤 / 𝑥 ] 𝜑 ) )
15	14	ralrimiva	⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑦 → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑦 → [ 𝑤 / 𝑥 ] 𝜑 ) )