Theorem ralbidv2 3155

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralbidva  3157  raleqbidv  3316  ralssOLD  4010  oneqmini  6370  ordunisuc2  7786  dfsmo2  8279  wemapsolem  9455  zorn2lem1  10406  raluz  12809  limsupgle  15400  ello12  15439  elo12  15450  lo1resb  15487  rlimresb  15488  o1resb  15489  isprm3  16610  isprm7  16635  ist1-2  23291  hausdiag  23589  xkopt  23599  cnflf  23946  cnfcf  23986  metcnp  24485  caucfil  25239  mdegleb  26025  islinds5  33448  islbs5  33461  eulerpartlemgvv  34533  filnetlem4  36575  mnuunid  44528  iineq12dv  45360  hoidmvle  46854  elbigo2  48808  ralbidb  49055  ralbidc  49056