Theorem 2ralbidva 3224

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  disjxun  5101  reu3op  6290  opreu2reurex  6292  isocnv3  7333  isotr  7337  f1oweALT  7969  fnmpoovd  8084  pospropd  18413  tosso  18505  isipodrs  18625  mgmpropd  18743  mgmhmpropd  18800  sgrppropd  18833  mndpropd  18864  mhmpropd  18900  efgred  19875  cmnpropd  19918  rngpropd  20309  ringpropd  20430  isdomn3  20876  lmodprop2d  21108  lsspropd  21201  islmhm2  21222  lmhmpropd  21257  df2idl2crng  21484  islindf4  22051  assapropd  22086  scmatmats  22733  cpmatel2  22938  1elcpmat  22940  m2cpminvid2  22980  decpmataa0  22993  pmatcollpw2lem  23002  connsub  23646  hausdiag  23871  ist0-4  23955  ismet2  24559  txmetcnp  24773  txmetcn  24774  metuel2  24791  metucn  24797  isngp3  24824  nlmvscn  24913  isclmp  25325  isncvsngp  25377  ipcn  25474  iscfil2  25494  caucfil  25511  cfilresi  25523  ulmdvlem3  26638  cxpcn3  26985  tgjustf  28814  tgjustr  28815  tgcgr4  28873  perpcom  29067  brbtwn2  29362  colinearalglem2  29364  eengtrkg  29443  isarchi2  33625  opprlidlabs  33887  elmrsubrn  36099  nmulprop  36770  nmulcom  36774  nadddilem2  36801  nadddilem4  36803  isbnd3b  38535  iscvlat2N  40197  ishlat3N  40227  gicabl  43940  lindslinindsimp2  49393  joindm3  49895  meetdm3  49897  fucofulem2  50237  thincpropd  50368  functhinclem1  50370  fulltermc  50437  postc  50495  islmd  50591  iscmd  50592