Theorem 2ralbii 3111

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

Syntax hints:   ↔ wb 206  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ral 3052

This theorem is referenced by:  3ralbii  3113  ralnex3  3117  rmo4f  3693  2reu4lem  4476  cnvso  6246  fununi  6567  dff14a  7216  isocnv2  7277  f1opr  7414  sorpss  7673  xpord3inddlem  8096  tpossym  8200  dford2  9529  isffth2  17842  ispos2  18238  issubmgm  18627  issubm  18728  cntzrec  19265  oppgsubm  19291  opprirred  20358  opprsubrng  20492  rhmimasubrng  20499  cntzsubrng  20500  opprsubrg  20526  isdomn5  20643  isdomn3  20648  gsummatr01lem3  22601  gsummatr01  22603  isbasis2g  22892  ist0-3  23289  isfbas2  23779  isclmp  25053  addsproplem4  27968  addsproplem6  27970  addsprop  27972  negsproplem4  28027  negsproplem6  28029  negsprop  28031  mulsprop  28126  dfadj2  31960  adjval2  31966  cnlnadjeui  32152  adjbdln  32158  isarchi  33264  prmidl0  33531  ply1dg3rt0irred  33665  dff15  35240  iccllysconn  35444  dfso3  35914  elpotr  35973  dfon2  35984  idinxpss  38511  inxpssidinxp  38515  idinxpssinxp  38516  dfeldisj5  38980  isltrn2N  40380  hashnexinj  42382  fphpd  43058  fiinfi  43814  ntrk1k3eqk13  44291  ordelordALT  44778  dfac5prim  45231  disjinfi  45436  isthinc2  49665  isthinc3  49666