Theorem ralbidv2 3153

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

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

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 3050

This theorem is referenced by:  ralbidva  3155  raleqbidv  3314  ralssOLD  4008  oneqmini  6368  ordunisuc2  7784  dfsmo2  8277  wemapsolem  9453  zorn2lem1  10404  raluz  12807  limsupgle  15398  ello12  15437  elo12  15448  lo1resb  15485  rlimresb  15486  o1resb  15487  isprm3  16608  isprm7  16633  ist1-2  23289  hausdiag  23587  xkopt  23597  cnflf  23944  cnfcf  23984  metcnp  24483  caucfil  25237  mdegleb  26023  islinds5  33397  islbs5  33410  eulerpartlemgvv  34482  filnetlem4  36524  mnuunid  44460  iineq12dv  45292  hoidmvle  46786  elbigo2  48740  ralbidb  48987  ralbidc  48988