Theorem 2ralbii 3137

Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Hypothesis

Ref	Expression
2ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2ralbii	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralbii

Step	Hyp	Ref	Expression
1		2ralbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	ralbii 3108	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3108	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   ↔ wb 209  ∀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

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

This theorem is used by:  3ralbii  3139  ralnex3  3143  rmo4f  3693  2reu4lem  4479  cnvso  6286  fununi  6608  dff14a  7267  dff15  7269  isocnv2  7332  f1opr  7469  sorpss  7729  xpord3inddlem  8152  tpossym  8256  dford2  9599  isffth2  18007  ispos2  18403  issubmgm  18804  issubm  18911  cntzrec  19463  oppgsubm  19489  opprirred  20563  opprsubrng  20721  rhmimasubrng  20728  cntzsubrng  20729  opprsubrg  20755  isdomn5  20872  isdomn3  20876  prmidl0  21541  gsummatr01lem3  22879  gsummatr01  22881  isbasis2g  23173  ist0-3  23570  isfbas2  24061  isclmp  25325  addsproplem4  28237  addsproplem6  28239  addsprop  28241  negsproplem4  28296  negsproplem6  28298  negsprop  28300  mulsprop  28395  dfadj2  32366  adjval2  32372  cnlnadjeui  32558  adjbdln  32564  isarchi  33622  ply1dg3rt0irred  33994  iccllysconn  35829  dfso3  36299  elpotr  36358  dfon2  36369  idinxpss  39066  inxpssidinxp  39070  idinxpssinxp  39071  dfdisjALTV5a  39551  dfeldisj5  39561  dfeldisj5a  39562  isltrn2N  40993  hashnexinj  42994  fphpd  43657  fiinfi  44413  ntrk1k3eqk13  44890  ordelordALT  45360  dfac5prim  45813  disjinfi  46024  isthinc2  50346  isthinc3  50347