![]() |
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 2370 | . 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 2370 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∃wrex 2350 |
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 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-rex 2355 |
This theorem is referenced by: f1oiso 5496 elrnmpt2g 5644 elrnmpt2 5645 ralrnmpt2 5646 rexrnmpt2 5647 ovelrn 5680 eroveu 6263 genipv 6761 genpelxp 6763 genpelvl 6764 genpelvu 6765 axcnre 7109 apreap 7754 apreim 7770 bezoutlemnewy 10529 bezoutlema 10532 bezoutlemb 10533 |
Copyright terms: Public domain | W3C validator |