Theorem 2ralsng

Description: Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019)

	Ref	Expression
Hypotheses	ralsng.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	2ralsng.1	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
Assertion	2ralsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝜑 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralsng.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		2ralsng.1	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3	1	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ { 𝐵 } 𝜑 ↔ ∀ 𝑦 ∈ { 𝐵 } 𝜓 ) )
4	3	ralsng	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝜑 ↔ ∀ 𝑦 ∈ { 𝐵 } 𝜓 ) )
5	2	ralsng	⊢ ( 𝐵 ∈ 𝑊 → ( ∀ 𝑦 ∈ { 𝐵 } 𝜓 ↔ 𝜒 ) )
6	4 5	sylan9bb	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝜑 ↔ 𝜒 ) )