![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexralbidv | GIF version |
Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rexralbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | ralbidv 2490 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 2491 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wral 2468 ∃wrex 2469 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 df-rex 2474 |
This theorem is referenced by: caucvgpr 7716 caucvgprpr 7746 caucvgsrlemgt1 7829 caucvgsrlemoffres 7834 axcaucvglemres 7933 cvg1nlemres 11035 rexfiuz 11039 resqrexlemgt0 11070 resqrexlemoverl 11071 resqrexlemglsq 11072 resqrexlemsqa 11074 resqrexlemex 11075 cau3lem 11164 caubnd2 11167 climi 11336 2clim 11350 ennnfonelemim 12486 lmcvg 14202 lmss 14231 txlm 14264 metcnpi 14500 metcnpi2 14501 elcncf 14545 cncfi 14550 limcimo 14619 cnplimclemr 14623 limccoap 14632 |
Copyright terms: Public domain | W3C validator |