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

Metamath Proof Explorer

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 ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ∀ 𝑦 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝜑 ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ( ∀ 𝑦 ∈ 𝐴 𝜒 ∧ 𝜃 ) ) ) )