Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > reeanv | GIF version |
Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.) |
Ref | Expression |
---|---|
reeanv | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1508 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1508 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | 1, 2 | reean 2599 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wrex 2417 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 |
This theorem is referenced by: 3reeanv 2601 fliftfun 5697 tfrlem5 6211 eroveu 6520 erovlem 6521 xpf1o 6738 genprndl 7336 genprndu 7337 ltpopr 7410 ltsopr 7411 cauappcvgprlemdisj 7466 caucvgprlemdisj 7489 caucvgprprlemdisj 7517 exbtwnzlemex 10034 rebtwn2z 10039 rexanre 10999 summodc 11159 prodmodclem2 11353 prodmodc 11354 dvds2lem 11512 odd2np1 11577 opoe 11599 omoe 11600 opeo 11601 omeo 11602 gcddiv 11714 divgcdcoprmex 11790 tgcl 12243 restbasg 12347 txuni2 12435 txbas 12437 txcnp 12450 blin2 12611 tgqioo 12726 |
Copyright terms: Public domain | W3C validator |