Theorem 2ralbii 3125

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

Syntax hints:   ↔ wb 205  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralnex3  3129  rmo4f  3688  2reu4lem  4478  cnvso  6233  fununi  6568  dff14a  7208  isocnv2  7267  f1opr  7402  sorpss  7652  tpossym  8153  dford2  9486  isffth2  17734  ispos2  18135  issubm  18544  cntzrec  19041  oppgsubm  19070  opprirred  20043  opprsubrg  20154  gsummatr01lem3  21916  gsummatr01  21918  isbasis2g  22208  ist0-3  22606  isfbas2  23096  isclmp  24370  dfadj2  30601  adjval2  30607  cnlnadjeui  30793  adjbdln  30799  isarchi  31787  prmidl0  31987  dff15  33419  iccllysconn  33575  dfso3  34024  elpotr  34104  dfon2  34115  xpord3ind  34146  addsproplem4  34238  addsproplem6  34240  addsprop  34242  3ralbii  36564  idinxpss  36629  inxpssidinxp  36633  idinxpssinxp  36634  dfeldisj5  37039  isltrn2N  38439  isdomn5  40479  fphpd  40951  isdomn3  41343  fiinfi  41554  ntrk1k3eqk13  42033  ordelordALT  42530  disjinfi  43110  issubmgm  45761  isthinc2  46720  isthinc3  46721