Theorem 2ralbidva 3200

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 3159	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralbidva 3159	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  5084  reu3op  6248  opreu2reurex  6250  isocnv3  7278  isotr  7282  f1oweALT  7916  fnmpoovd  8028  pospropd  18280  tosso  18372  isipodrs  18492  mgmpropd  18608  mgmhmpropd  18655  sgrppropd  18688  mndpropd  18716  mhmpropd  18749  efgred  19712  cmnpropd  19755  rngpropd  20144  ringpropd  20258  isdomn3  20681  lmodprop2d  20908  lsspropd  21002  islmhm2  21023  lmhmpropd  21058  islindf4  21826  assapropd  21859  scmatmats  22485  cpmatel2  22687  1elcpmat  22689  m2cpminvid2  22729  decpmataa0  22742  pmatcollpw2lem  22751  connsub  23395  hausdiag  23619  ist0-4  23703  ismet2  24307  txmetcnp  24521  txmetcn  24522  metuel2  24539  metucn  24545  isngp3  24572  nlmvscn  24661  isclmp  25073  isncvsngp  25125  ipcn  25222  iscfil2  25242  caucfil  25259  cfilresi  25271  ulmdvlem3  26382  cxpcn3  26729  tgjustf  28560  tgjustr  28561  tgcgr4  28618  perpcom  28800  brbtwn2  28993  colinearalglem2  28995  eengtrkg  29074  isarchi2  33266  opprlidlabs  33565  elmrsubrn  35723  isbnd3b  38117  iscvlat2N  39781  ishlat3N  39811  gicabl  43542  lindslinindsimp2  48936  joindm3  49441  meetdm3  49443  fucofulem2  49783  thincpropd  49914  functhinclem1  49916  fulltermc  49983  postc  50041  islmd  50137  iscmd  50138