Theorem 2ralbidva 3215

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 3174	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3174	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2105  ∀wral 3060

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3061

This theorem is referenced by:  disjxun  5147  reu3op  6292  opreu2reurex  6294  isocnv3  7332  isotr  7336  f1oweALT  7962  fnmpoovd  8076  pospropd  18285  tosso  18377  isipodrs  18495  mgmpropd  18577  mgmhmpropd  18624  sgrppropd  18657  mndpropd  18685  mhmpropd  18715  efgred  19658  cmnpropd  19701  rngpropd  20069  ringpropd  20177  lmodprop2d  20679  lsspropd  20773  islmhm2  20794  lmhmpropd  20829  islindf4  21613  assapropd  21646  scmatmats  22234  cpmatel2  22436  1elcpmat  22438  m2cpminvid2  22478  decpmataa0  22491  pmatcollpw2lem  22500  connsub  23146  hausdiag  23370  ist0-4  23454  ismet2  24060  txmetcnp  24277  txmetcn  24278  metuel2  24295  metucn  24301  isngp3  24328  nlmvscn  24425  isclmp  24845  isncvsngp  24898  ipcn  24995  iscfil2  25015  caucfil  25032  cfilresi  25044  ulmdvlem3  26147  cxpcn3  26489  tgjustf  27988  tgjustr  27989  tgcgr4  28046  perpcom  28228  brbtwn2  28427  colinearalglem2  28429  eengtrkg  28508  isarchi2  32598  opprlidlabs  32870  elmrsubrn  34806  isbnd3b  36957  iscvlat2N  38498  ishlat3N  38528  gicabl  42144  isdomn3  42249  lindslinindsimp2  47233  joindm3  47691  meetdm3  47693  functhinclem1  47750  postc  47791