Theorem ralbidv2 3190

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  ralbidva  3192  raleqbidv  3345  ralssOLD  4020  oneqmini  6415  ordunisuc2  7840  dfsmo2  8334  wemapsolem  9512  zorn2lem1  10480  raluz  12920  limsupgle  15528  ello12  15567  elo12  15578  lo1resb  15615  rlimresb  15616  o1resb  15617  isprm3  16741  isprm7  16767  ist1-2  23473  hausdiag  23771  xkopt  23781  cnflf  24128  cnfcf  24168  metcnp  24667  caucfil  25411  mdegleb  26190  islinds5  33625  islbs5  33637  eulerpartlemgvv  34711  filnetlem4  36781  mnuunid  44879  iineq12dv  45716  hoidmvle  47206  elbigo2  49217  ralbidb  49463  ralbidc  49464