Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2rexbidv | GIF version |
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | rexbidv 2369 | . 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 2369 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∃wrex 2349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-rex 2354 |
This theorem is referenced by: f1oiso 5485 elrnmpt2g 5633 elrnmpt2 5634 ralrnmpt2 5635 rexrnmpt2 5636 ovelrn 5669 eroveu 6220 genipv 6699 genpelxp 6701 genpelvl 6702 genpelvu 6703 axcnre 7047 apreap 7687 apreim 7703 bezoutlemnewy 10385 bezoutlema 10388 bezoutlemb 10389 |
Copyright terms: Public domain | W3C validator |