Theorem ralbidv2 3173

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem ralbidv2

Step	Hyp	Ref	Expression
1		ralbidv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒)))
2	1	albidv 1923	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)))
3		df-ral 3062	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 3062	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))
5	2, 3, 4	3bitr4g 313	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ral 3062

This theorem is referenced by:  ralbidva  3175  raleqbidv  3342  ralss  4054  oneqmini  6416  ordunisuc2  7835  dfsmo2  8349  wemapsolem  9547  zorn2lem1  10493  raluz  12882  limsupgle  15423  ello12  15462  elo12  15473  lo1resb  15510  rlimresb  15511  o1resb  15512  isprm3  16622  isprm7  16647  ist1-2  22858  hausdiag  23156  xkopt  23166  cnflf  23513  cnfcf  23553  metcnp  24057  caucfil  24807  mdegleb  25589  islinds5  32525  islbs5  32541  eulerpartlemgvv  33444  filnetlem4  35352  mnuunid  43118  hoidmvle  45395  elbigo2  47316  ralbidb  47563  ralbidc  47564