Theorem ralbidv2 3111

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 1924	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)))
3		df-ral 3070	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 3070	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  ralbidva  3112  raleqbidv  3337  ralss  3992  oneqmini  6321  ordunisuc2  7700  dfsmo2  8187  wemapsolem  9318  zorn2lem1  10261  raluz  12645  limsupgle  15195  ello12  15234  elo12  15245  lo1resb  15282  rlimresb  15283  o1resb  15284  isprm3  16397  isprm7  16422  ist1-2  22507  hausdiag  22805  xkopt  22815  cnflf  23162  cnfcf  23202  metcnp  23706  caucfil  24456  mdegleb  25238  islinds5  31572  eulerpartlemgvv  32352  filnetlem4  34579  mnuunid  41902  hoidmvle  44145  elbigo2  45909  ralbidb  46156  ralbidc  46157