Theorem reeanv 2647

Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		nfv 1528	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 2646	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wrex 2456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461

This theorem is referenced by:  3reeanv  2648  fliftfun  5799  tfrlem5  6317  eroveu  6628  erovlem  6629  xpf1o  6846  genprndl  7522  genprndu  7523  ltpopr  7596  ltsopr  7597  cauappcvgprlemdisj  7652  caucvgprlemdisj  7675  caucvgprprlemdisj  7703  exbtwnzlemex  10252  rebtwn2z  10257  rexanre  11231  summodc  11393  prodmodclem2  11587  prodmodc  11588  dvds2lem  11812  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  gcddiv  12022  divgcdcoprmex  12104  pcqmul  12305  pcadd  12341  mul4sq  12394  dvdsrtr  13275  unitgrp  13290  lss1d  13475  tgcl  13649  restbasg  13753  txuni2  13841  txbas  13843  txcnp  13856  blin2  14017  tgqioo  14132  mul2sq  14548  2sqlem5  14551