Theorem bj-ralvw

Description: A weak version of ralv not using ax-ext (nor df-cleq , df-clel , df-v ), and only core FOL axioms. See also bj-rexvw . The analogues for reuv and rmov are not proved. (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-ralvw.1	⊢ 𝜓
Assertion	bj-ralvw	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜓 } 𝜑 ↔ ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bj-ralvw.1	⊢ 𝜓
2		df-ral	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜓 } 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ 𝜓 } → 𝜑 ) )
3	1	vexw	⊢ 𝑥 ∈ { 𝑦 ∣ 𝜓 }
4	3	a1bi	⊢ ( 𝜑 ↔ ( 𝑥 ∈ { 𝑦 ∣ 𝜓 } → 𝜑 ) )
5	4	albii	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ 𝜓 } → 𝜑 ) )
6	2 5	bitr4i	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜓 } 𝜑 ↔ ∀ 𝑥 𝜑 )