Theorem raleqbidv 2709

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)

Hypotheses

Ref	Expression
raleqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
raleqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
raleqbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem raleqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	raleqdv 2699	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 2497	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  ∀wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480

This theorem is referenced by:  rspc2vd  3153  ofrfval  6144  fmpox  6258  tfrlemi1  6390  supeq123d  7057  cvg1nlemcau  11149  cvg1nlemres  11150  cau3lem  11279  fsum2dlemstep  11599  fisumcom2  11603  fprod2dlemstep  11787  fprodcom2fi  11791  pcfac  12519  ptex  12935  prdsex  12940  ismgm  13000  mgm1  13013  grpidvalg  13016  gsumress  13038  issgrp  13046  sgrp1  13054  sgrppropd  13056  ismnddef  13059  ismndd  13078  mndpropd  13081  mnd1  13087  ismhm  13093  mhmex  13094  resmhm  13119  isgrp  13138  grppropd  13149  isgrpd2e  13152  grp1  13238  isnsg  13332  nmznsg  13343  isghm  13373  cmnpropd  13425  iscmnd  13428  isrng  13490  rngpropd  13511  dfur2g  13518  issrg  13521  issrgid  13537  isring  13556  iscrng2  13571  ringideu  13573  isringid  13581  ringpropd  13594  ring1  13615  oppr0g  13637  oppr1g  13638  isrhm2d  13721  rhmopp  13732  islring  13748  rrgval  13818  isdomn  13825  opprdomnbg  13830  islmod  13847  islmodd  13849  lmodprop2d  13904  lsssetm  13912  islidlm  14035  rnglidlmmgm  14052  rnglidlmsgrp  14053  istopg  14235  restbasg  14404  cnfval  14430  cnpfval  14431  txbas  14494  limccl  14895  sscoll2  15634