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 2438 | . 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 2438 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-rex 2422 |
This theorem is referenced by: f1oiso 5727 elrnmpog 5883 elrnmpo 5884 ralrnmpo 5885 rexrnmpo 5886 ovelrn 5919 eroveu 6520 genipv 7317 genpelxp 7319 genpelvl 7320 genpelvu 7321 axcnre 7689 apreap 8349 apreim 8365 aprcl 8408 bezoutlemnewy 11684 bezoutlema 11687 bezoutlemb 11688 txuni2 12425 txbas 12427 txdis1cn 12447 |
Copyright terms: Public domain | W3C validator |