Theorem 2ralbidva 3225

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.)

Hypothesis

Ref	Expression
2ralbidva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2ralbidva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴

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

Proof of Theorem 2ralbidva

Step	Hyp	Ref	Expression
1		2ralbidva.1	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))
2	1	anassrs 467	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒))
3	2	ralbidva 3182	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3182	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3068

This theorem is referenced by:  disjxun  5164  reu3op  6323  opreu2reurex  6325  isocnv3  7368  isotr  7372  f1oweALT  8013  fnmpoovd  8128  pospropd  18397  tosso  18489  isipodrs  18607  mgmpropd  18689  mgmhmpropd  18736  sgrppropd  18769  mndpropd  18797  mhmpropd  18827  efgred  19790  cmnpropd  19833  rngpropd  20201  ringpropd  20311  isdomn3  20737  lmodprop2d  20944  lsspropd  21039  islmhm2  21060  lmhmpropd  21095  islindf4  21881  assapropd  21915  scmatmats  22538  cpmatel2  22740  1elcpmat  22742  m2cpminvid2  22782  decpmataa0  22795  pmatcollpw2lem  22804  connsub  23450  hausdiag  23674  ist0-4  23758  ismet2  24364  txmetcnp  24581  txmetcn  24582  metuel2  24599  metucn  24605  isngp3  24632  nlmvscn  24729  isclmp  25149  isncvsngp  25202  ipcn  25299  iscfil2  25319  caucfil  25336  cfilresi  25348  ulmdvlem3  26463  cxpcn3  26809  tgjustf  28499  tgjustr  28500  tgcgr4  28557  perpcom  28739  brbtwn2  28938  colinearalglem2  28940  eengtrkg  29019  isarchi2  33165  opprlidlabs  33478  elmrsubrn  35488  isbnd3b  37745  iscvlat2N  39280  ishlat3N  39310  gicabl  43056  lindslinindsimp2  48192  joindm3  48649  meetdm3  48651  functhinclem1  48708  postc  48749