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  5797  tfrlem5  6315  eroveu  6626  erovlem  6627  xpf1o  6844  genprndl  7520  genprndu  7521  ltpopr  7594  ltsopr  7595  cauappcvgprlemdisj  7650  caucvgprlemdisj  7673  caucvgprprlemdisj  7701  exbtwnzlemex  10250  rebtwn2z  10255  rexanre  11229  summodc  11391  prodmodclem2  11585  prodmodc  11586  dvds2lem  11810  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  gcddiv  12020  divgcdcoprmex  12102  pcqmul  12303  pcadd  12339  mul4sq  12392  dvdsrtr  13270  unitgrp  13285  tgcl  13567  restbasg  13671  txuni2  13759  txbas  13761  txcnp  13774  blin2  13935  tgqioo  14050  mul2sq  14466  2sqlem5  14469