Theorem 2ralbidva 3203

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  disjxun  5073  reu3op  6247  opreu2reurex  6249  isocnv3  7280  isotr  7284  f1oweALT  7918  fnmpoovd  8030  pospropd  18286  tosso  18378  isipodrs  18498  mgmpropd  18614  mgmhmpropd  18661  sgrppropd  18694  mndpropd  18722  mhmpropd  18755  efgred  19718  cmnpropd  19761  rngpropd  20150  ringpropd  20264  isdomn3  20691  lmodprop2d  20918  lsspropd  21011  islmhm2  21032  lmhmpropd  21067  islindf4  21817  assapropd  21850  scmatmats  22498  cpmatel2  22700  1elcpmat  22702  m2cpminvid2  22742  decpmataa0  22755  pmatcollpw2lem  22764  connsub  23408  hausdiag  23632  ist0-4  23716  ismet2  24320  txmetcnp  24534  txmetcn  24535  metuel2  24552  metucn  24558  isngp3  24585  nlmvscn  24674  isclmp  25086  isncvsngp  25138  ipcn  25235  iscfil2  25255  caucfil  25272  cfilresi  25284  ulmdvlem3  26389  cxpcn3  26734  tgjustf  28563  tgjustr  28564  tgcgr4  28621  perpcom  28803  brbtwn2  28996  colinearalglem2  28998  eengtrkg  29077  isarchi2  33270  opprlidlabs  33572  elmrsubrn  35763  isbnd3b  38167  iscvlat2N  39831  ishlat3N  39861  gicabl  43559  lindslinindsimp2  48968  joindm3  49473  meetdm3  49475  fucofulem2  49815  thincpropd  49946  functhinclem1  49948  fulltermc  50015  postc  50073  islmd  50169  iscmd  50170