Theorem 2ralbidva 3199

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  disjxun  5097  reu3op  6251  opreu2reurex  6253  isocnv3  7280  isotr  7284  f1oweALT  7918  fnmpoovd  8031  pospropd  18252  tosso  18344  isipodrs  18464  mgmpropd  18580  mgmhmpropd  18627  sgrppropd  18660  mndpropd  18688  mhmpropd  18721  efgred  19681  cmnpropd  19724  rngpropd  20113  ringpropd  20227  isdomn3  20652  lmodprop2d  20879  lsspropd  20973  islmhm2  20994  lmhmpropd  21029  islindf4  21797  assapropd  21831  scmatmats  22459  cpmatel2  22661  1elcpmat  22663  m2cpminvid2  22703  decpmataa0  22716  pmatcollpw2lem  22725  connsub  23369  hausdiag  23593  ist0-4  23677  ismet2  24281  txmetcnp  24495  txmetcn  24496  metuel2  24513  metucn  24519  isngp3  24546  nlmvscn  24635  isclmp  25057  isncvsngp  25109  ipcn  25206  iscfil2  25226  caucfil  25243  cfilresi  25255  ulmdvlem3  26371  cxpcn3  26718  tgjustf  28549  tgjustr  28550  tgcgr4  28607  perpcom  28789  brbtwn2  28982  colinearalglem2  28984  eengtrkg  29063  isarchi2  33269  opprlidlabs  33568  elmrsubrn  35716  isbnd3b  37988  iscvlat2N  39652  ishlat3N  39682  gicabl  43408  lindslinindsimp2  48776  joindm3  49281  meetdm3  49283  fucofulem2  49623  thincpropd  49754  functhinclem1  49756  fulltermc  49823  postc  49881  islmd  49977  iscmd  49978