Theorem ralbii2 3095

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 1817	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
3		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
5	2, 3, 4	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207  df-ral 3068

This theorem is referenced by:  ralbiia  3097  ralcom3  3103  raleqbii  3352  ralrab  3715  raldifb  4172  raldifsni  4820  reusv2  5421  dfsup2  9513  iscard2  10045  acnnum  10121  dfac9  10206  dfacacn  10211  raluz2  12962  ralrp  13077  isprm4  16731  isdomn2OLD  20734  sdrgacs  20824  isnrm2  23387  ismbl  25580  ellimc3  25934  dchrelbas2  27299  h1dei  31582  iineq1i  36160  ixpeq1i  36164  ralin  38204  fnwe2lem2  43008