![]() |
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 form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | rexbidv 2478 | . 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 2478 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-rex 2461 |
This theorem is referenced by: f1oiso 5820 elrnmpog 5980 elrnmpo 5981 ralrnmpo 5982 rexrnmpo 5983 ovelrn 6016 eroveu 6619 genipv 7486 genpelxp 7488 genpelvl 7489 genpelvu 7490 axcnre 7858 apreap 8521 apreim 8537 aprcl 8580 bezoutlemnewy 11967 bezoutlema 11970 bezoutlemb 11971 pythagtriplem19 12252 pceu 12265 pcval 12266 pczpre 12267 pcdiv 12272 4sqlem2 12357 4sqlem3 12358 4sqlem4 12360 txuni2 13389 txbas 13391 txdis1cn 13411 2sqlem2 14084 2sqlem8 14092 2sqlem9 14093 |
Copyright terms: Public domain | W3C validator |