Theorem 2ralbidva 3228

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

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

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 1945

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

This theorem is used by:  disjxun  5104  reu3op  6310  opreu2reurex  6312  isocnv3  7360  isotr  7364  f1oweALT  8005  fnmpoovd  8120  pospropd  18525  tosso  18617  isipodrs  18737  mgmpropd  18855  mgmhmpropd  18913  sgrppropd  18946  mndpropd  18977  mhmpropd  19013  efgred  19989  cmnpropd  20032  rngpropd  20423  ringpropd  20546  isdomn3  20993  lmodprop2d  21226  lsspropd  21319  islmhm2  21340  lmhmpropd  21375  df2idl2crng  21604  islindf4  22171  assapropd  22206  scmatmats  22853  cpmatel2  23058  1elcpmat  23060  m2cpminvid2  23100  decpmataa0  23113  pmatcollpw2lem  23122  connsub  23766  hausdiag  23991  ist0-4  24075  ismet2  24679  txmetcnp  24893  txmetcn  24894  metuel2  24911  metucn  24917  isngp3  24944  nlmvscn  25033  isclmp  25445  isncvsngp  25497  ipcn  25594  iscfil2  25614  caucfil  25631  cfilresi  25643  ulmdvlem3  26756  cxpcn3  27103  tgjustf  28962  tgjustr  28963  tgcgr4  29021  perpcom  29215  brbtwn2  29510  colinearalglem2  29512  eengtrkg  29591  isarchi2  33813  opprlidlabs  34076  elmrsubrn  36451  nmulprop  37116  nmulcom  37120  nadddilem2  37147  nadddilem4  37149  isbnd3b  38910  iscvlat2N  40572  ishlat3N  40602  gicabl  44292  lindslinindsimp2  49778  joindm3  50286  meetdm3  50288  fucofulem2  50636  thincpropd  50780  functhinclem1  50782  fulltermc  50849  postc  50910  islmd  51051  iscmd  51052