Theorem 2ralbii 3138

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 3109	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3109	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   ↔ wb 209  ∀wral 3077

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 3078

This theorem is used by:  3ralbii  3140  ralnex3  3144  rmo4f  3693  2reu4lem  4479  cnvso  6290  fununi  6613  dff14a  7272  dff15  7274  isocnv2  7337  f1opr  7474  sorpss  7742  xpord3inddlem  8164  tpossym  8268  dford2  9614  isffth2  18086  ispos2  18482  issubmgm  18884  issubm  18991  cntzrec  19543  oppgsubm  19569  dfring3  20511  opprirred  20645  opprsubrng  20804  rhmimasubrng  20811  cntzsubrng  20812  opprsubrg  20838  isdomn5  20955  isdomn3  20959  prmidl0  21627  gsummatr01lem3  22965  gsummatr01  22967  isbasis2g  23259  ist0-3  23656  isfbas2  24147  isclmp  25411  addsproplem4  28351  addsproplem6  28353  addsprop  28355  negsproplem4  28410  negsproplem6  28412  negsprop  28414  mulsprop  28509  dfadj2  32480  adjval2  32486  cnlnadjeui  32672  adjbdln  32678  isarchi  33736  ply1dg3rt0irred  34109  iccllysconn  35994  dfso3  36464  elpotr  36523  dfon2  36534  idinxpss  39230  inxpssidinxp  39234  idinxpssinxp  39235  dfdisjALTV5a  39715  dfeldisj5  39725  dfeldisj5a  39726  isltrn2N  41157  hashnexinj  43158  fphpd  43802  fiinfi  44558  ntrk1k3eqk13  45035  ordelordALT  45505  dfac5prim  45958  disjinfi  46176  isthinc2  50497  isthinc3  50498