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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  disjxun  5117  reu3op  6281  opreu2reurex  6283  isocnv3  7324  isotr  7328  f1oweALT  7969  fnmpoovd  8084  pospropd  18335  tosso  18427  isipodrs  18545  mgmpropd  18627  mgmhmpropd  18674  sgrppropd  18707  mndpropd  18735  mhmpropd  18768  efgred  19727  cmnpropd  19770  rngpropd  20132  ringpropd  20246  isdomn3  20673  lmodprop2d  20879  lsspropd  20973  islmhm2  20994  lmhmpropd  21029  islindf4  21796  assapropd  21830  scmatmats  22447  cpmatel2  22649  1elcpmat  22651  m2cpminvid2  22691  decpmataa0  22704  pmatcollpw2lem  22713  connsub  23357  hausdiag  23581  ist0-4  23665  ismet2  24270  txmetcnp  24484  txmetcn  24485  metuel2  24502  metucn  24508  isngp3  24535  nlmvscn  24624  isclmp  25046  isncvsngp  25099  ipcn  25196  iscfil2  25216  caucfil  25233  cfilresi  25245  ulmdvlem3  26361  cxpcn3  26708  tgjustf  28398  tgjustr  28399  tgcgr4  28456  perpcom  28638  brbtwn2  28830  colinearalglem2  28832  eengtrkg  28911  isarchi2  33129  opprlidlabs  33446  elmrsubrn  35488  isbnd3b  37755  iscvlat2N  39288  ishlat3N  39318  gicabl  43070  lindslinindsimp2  48387  joindm3  48891  meetdm3  48893  fucofulem2  49170  thincpropd  49276  functhinclem1  49278  fulltermc  49344  postc  49394  islmd  49483  iscmd  49484