Theorem 2ralunsn

Description: Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012)

	Ref	Expression
Hypotheses	2ralunsn.1	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
	2ralunsn.2	⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
	2ralunsn.3	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜃 ) )
Assertion	2ralunsn	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝜑 ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2ralunsn.1	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
2		2ralunsn.2	⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
3		2ralunsn.3	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜃 ) )
4	2	ralunsn	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝜑 ↔ ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ) )
5	4	ralbidv	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝜑 ↔ ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ) )
6	1	ralbidv	⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜒 ) )
7	6 3	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) )
8	7	ralunsn	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) ) )
9		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
10	9	anbi1i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) )
11	8 10	bitrdi	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ( ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝜓 ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) ) )
12	5 11	bitrd	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝜑 ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) ) )