Theorem ralbii2 3105

Description: Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)

Hypothesis

Ref	Expression
ralbii2.1	⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓))

Assertion

Ref	Expression
ralbii2	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)

Proof of Theorem ralbii2

Step	Hyp	Ref	Expression
1		ralbii2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓))
2	1	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
3		df-ral 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3078	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
5	2, 3, 4	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  ralbiia  3107  ralcom3  3113  raleqbii  3333  ralrab  3652  raldifb  4096  ralin  4195  raldifsni  4758  reusv2  5365  dfsup2  9429  iscard2  10050  acnnum  10124  dfac9  10208  dfacacn  10213  raluz2  13017  ralrp  13135  isprm4  16852  sdrgacs  21051  isnrm2  23669  ismbl  25840  ellimc3  26192  dchrelbas2  27557  onsis  28653  ons2ind  28654  h1dei  32145  iineq1i  36965  ixpeq1i  36969  fnwe2lem2  44037